diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-18 12:43:08 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-18 12:43:08 +0000 |
| commit | 512a76bd9b063f218822a4d3a885aa0b7bec347f (patch) | |
| tree | 2463ded34c93decc4a03077f82be42fa3f30f13d /contrib/romega/README | |
| parent | bc92d03704339465160b698bab152f238b92eadd (diff) | |
Romega/names/Makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/romega/README')
| -rw-r--r-- | contrib/romega/README | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/contrib/romega/README b/contrib/romega/README new file mode 100644 index 000000000..c82087c7d --- /dev/null +++ b/contrib/romega/README @@ -0,0 +1,19 @@ +This work was done for the RNRT Project Calife. +As such it is distributed under the LGPL licence. + +Change the COQTOP variable in the Makefile and type make. +The caml compiler should be in your path. + +WARNING : there is a bug in the 7.0 production release that prevents +the compilation of the core ReflOmegaCore.v module. This development +will only work with the beta release and (hopefully) subsequent version +of Coq. + +A patch (patch-v7) contributed by D. Delahaye is included to correct the bug in +regular 7.0 versions. It must be applied in the 'parsing' directory. +Using it with a 7.0beta requires a few changes in const_omega.ml due to +some changes in the paths of modules. + +Report bugs to : + pierre.cregut@francetelecom.com + |