Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
clarus committed Oct 24, 2013
1 parent 2af3a52 commit 64ff3d1
Showing 1 changed file with 13 additions and 15 deletions.
28 changes: 13 additions & 15 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,36 +1,34 @@
===============================================================================
Cybele
======

Cybele

Coq as an interactive programming language with effects
*A Coq plugin for simpler proofs by reflection or OCaml certificates.*

http://cybele.gforge.inria.fr/

===============================================================================
[http://cybele.gforge.inria.fr/](http://cybele.gforge.inria.fr/)

Requirements
============
------------

This plugin requires the latest trunk version of Coq.

Compilation
===========
-----------

Before anything else, make sure that all the utilities of Coq are in
your path. Compile by typing:

./configure.sh
make
./configure.sh
make

Finally, install your plugin:

make install
make install

(as root if necessary).

Examples
========
--------

Go to test-suite/. You can try out each example doing a:
./configure.sh
make

./configure.sh
make

0 comments on commit 64ff3d1

Please sign in to comment.