summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commitff1dde8f1585c92dd69a9a41ad709f15ef8936da (patch)
treee7e87fb5d549e0bf19785e54737a96ee4d9917d6
parenta788b511487e6b748d5be35140a7ad2ca110936e (diff)
parent4767d724d489a7ad67f696e9401e70b9f9ae2143 (diff)
Merge commit 'upstream/8.1.pl2+dfsg'
-rw-r--r--.depend130
-rw-r--r--CHANGES11
-rw-r--r--INSTALL49
-rw-r--r--INSTALL.ide79
-rw-r--r--INSTALL.win63
-rw-r--r--Makefile82
-rw-r--r--Makefile.dep2
-rw-r--r--PROBLEMES54
-rw-r--r--README.win34
-rw-r--r--TODO51
-rw-r--r--config/Makefile.template14
-rw-r--r--config/coq_config.mli3
-rwxr-xr-xconfigure267
-rw-r--r--contrib/cc/cctac.ml6
-rw-r--r--contrib/cc/cctac.mli4
-rw-r--r--contrib/extraction/extract_env.ml5
-rw-r--r--contrib/extraction/extraction.ml25
-rw-r--r--contrib/extraction/table.ml87
-rw-r--r--contrib/extraction/table.mli9
-rw-r--r--contrib/setoid_ring/Ring_tac.v9
-rw-r--r--contrib/setoid_ring/newring.ml47
-rw-r--r--dev/ocamldebug-coq.template6
-rw-r--r--doc/Makefile24
-rw-r--r--ide/command_windows.ml5
-rw-r--r--ide/coq.ml3
-rw-r--r--ide/coqide.ml41
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/coqlib.ml4
-rw-r--r--interp/coqlib.mli3
-rw-r--r--kernel/inductive.ml51
-rw-r--r--lib/compat.ml440
-rw-r--r--lib/options.ml4
-rw-r--r--lib/util.ml6
-rw-r--r--parsing/argextend.ml46
-rw-r--r--parsing/egrammar.mli6
-rw-r--r--parsing/g_vernac.ml46
-rw-r--r--parsing/g_xml.ml42
-rw-r--r--parsing/pcoq.ml429
-rw-r--r--parsing/pcoq.mli10
-rw-r--r--parsing/ppconstr.ml10
-rw-r--r--parsing/ppvernac.ml11
-rw-r--r--parsing/q_coqast.ml413
-rw-r--r--parsing/q_util.ml48
-rw-r--r--parsing/tacextend.ml44
-rw-r--r--parsing/vernacextend.ml44
-rw-r--r--pretyping/cases.ml14
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/tacred.ml39
-rw-r--r--scripts/coqmktop.ml9
-rw-r--r--tactics/setoid_replace.ml114
-rw-r--r--tactics/tacinterp.ml35
-rw-r--r--test-suite/success/cc.v19
-rw-r--r--tools/coq_makefile.ml410
-rw-r--r--tools/coqdep.ml26
-rw-r--r--tools/coqdoc/pretty.mll6
-rw-r--r--toplevel/command.ml54
-rw-r--r--toplevel/command.mli4
-rw-r--r--toplevel/metasyntax.ml8
-rw-r--r--toplevel/mltop.ml46
-rw-r--r--toplevel/toplevel.ml23
-rw-r--r--toplevel/vernacentries.ml5
-rw-r--r--toplevel/vernacexpr.ml3
-rw-r--r--toplevel/whelp.ml426
63 files changed, 1085 insertions, 613 deletions
diff --git a/.depend b/.depend
index e5787c82..f8aa692c 100644
--- a/.depend
+++ b/.depend
@@ -378,7 +378,8 @@ contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
kernel/names.cmi
contrib/cc/ccproof.cmi: kernel/term.cmi kernel/names.cmi \
contrib/cc/ccalgo.cmi
-contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi
+contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi \
+ contrib/cc/ccproof.cmi
contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \
kernel/term.cmi kernel/names.cmi
contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \
@@ -2261,8 +2262,9 @@ toplevel/command.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/typeops.cmi \
pretyping/indrec.cmi library/impargs.cmi library/global.cmi \
pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \
kernel/environ.cmi kernel/entries.cmi library/declare.cmi \
- kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \
- interp/constrextern.cmi toplevel/class.cmi toplevel/command.cmi
+ kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+ interp/constrintern.cmi interp/constrextern.cmi toplevel/class.cmi \
+ toplevel/command.cmi
toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \
interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
proofs/tacmach.cmx interp/syntax_def.cmx library/states.cmx \
@@ -2277,8 +2279,9 @@ toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \
pretyping/indrec.cmx library/impargs.cmx library/global.cmx \
pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \
kernel/environ.cmx kernel/entries.cmx library/declare.cmx \
- kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \
- interp/constrextern.cmx toplevel/class.cmx toplevel/command.cmi
+ kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+ interp/constrintern.cmx interp/constrextern.cmx toplevel/class.cmx \
+ toplevel/command.cmi
toplevel/coqinit.cmo: toplevel/vernac.cmi toplevel/toplevel.cmi \
lib/system.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \
library/nameops.cmi toplevel/mltop.cmi config/coq_config.cmi \
@@ -2483,18 +2486,20 @@ toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \
interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \
proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi library/nametab.cmi \
- kernel/names.cmi library/libnames.cmi parsing/lexer.cmi interp/genarg.cmi \
- kernel/environ.cmi parsing/egrammar.cmi library/dischargedhypsmap.cmi \
- pretyping/detyping.cmi interp/constrintern.cmi toplevel/command.cmi \
- toplevel/cerrors.cmi toplevel/whelp.cmi
+ kernel/names.cmi library/libnames.cmi parsing/lexer.cmi \
+ library/goptions.cmi interp/genarg.cmi kernel/environ.cmi \
+ parsing/egrammar.cmi library/dischargedhypsmap.cmi pretyping/detyping.cmi \
+ interp/constrintern.cmi toplevel/command.cmi toplevel/cerrors.cmi \
+ toplevel/whelp.cmi
toplevel/whelp.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx lib/system.cmx \
interp/syntax_def.cmx proofs/refiner.cmx pretyping/rawterm.cmx lib/pp.cmx \
proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx library/nametab.cmx \
- kernel/names.cmx library/libnames.cmx parsing/lexer.cmx interp/genarg.cmx \
- kernel/environ.cmx parsing/egrammar.cmx library/dischargedhypsmap.cmx \
- pretyping/detyping.cmx interp/constrintern.cmx toplevel/command.cmx \
- toplevel/cerrors.cmx toplevel/whelp.cmi
+ kernel/names.cmx library/libnames.cmx parsing/lexer.cmx \
+ library/goptions.cmx interp/genarg.cmx kernel/environ.cmx \
+ parsing/egrammar.cmx library/dischargedhypsmap.cmx pretyping/detyping.cmx \
+ interp/constrintern.cmx toplevel/command.cmx toplevel/cerrors.cmx \
+ toplevel/whelp.cmi
contrib/cc/ccalgo.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \
kernel/names.cmi library/goptions.cmi contrib/cc/ccalgo.cmi
contrib/cc/ccalgo.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \
@@ -3503,40 +3508,6 @@ contrib/omega/g_omega.cmx: lib/util.cmx tactics/tacinterp.cmx \
toplevel/cerrors.cmx
contrib/omega/omega.cmo: lib/util.cmi kernel/names.cmi
contrib/omega/omega.cmx: lib/util.cmx kernel/names.cmx
-contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \
- toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \
- kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
- kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
- proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \
- tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \
- pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
- pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \
- parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \
- library/nameops.cmi library/libnames.cmi library/lib.cmi \
- tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \
- pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \
- kernel/entries.cmi tactics/elim.cmi parsing/egrammar.cmi \
- tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \
- library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \
- toplevel/command.cmi kernel/closure.cmi toplevel/cerrors.cmi \
- tactics/auto.cmi
-contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx \
- toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \
- kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \
- kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \
- proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \
- tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/reductionops.cmx \
- pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
- pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \
- parsing/pcoq.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \
- library/nameops.cmx library/libnames.cmx library/lib.cmx \
- tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \
- pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \
- kernel/entries.cmx tactics/elim.cmx parsing/egrammar.cmx \
- tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \
- library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \
- toplevel/command.cmx kernel/closure.cmx toplevel/cerrors.cmx \
- tactics/auto.cmx
contrib/ring/g_quote.cmo: lib/util.cmi tactics/tacinterp.cmi \
proofs/tacexpr.cmo contrib/ring/quote.cmo parsing/pptactic.cmi lib/pp.cmi \
parsing/pcoq.cmi interp/genarg.cmi parsing/egrammar.cmi \
@@ -4001,6 +3972,10 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
parsing/egrammar.cmx toplevel/cerrors.cmx
contrib/xml/xml.cmo: contrib/xml/xml.cmi
contrib/xml/xml.cmx: contrib/xml/xml.cmi
+doc/refman/euclid.cmo: doc/refman/euclid.cmi
+doc/refman/euclid.cmx: doc/refman/euclid.cmi
+doc/refman/heapsort.cmo: doc/refman/heapsort.cmi
+doc/refman/heapsort.cmx: doc/refman/heapsort.cmi
ide/utils/config_file.cmo: ide/utils/config_file.cmi
ide/utils/config_file.cmx: ide/utils/config_file.cmi
ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \
@@ -4154,39 +4129,38 @@ tools/coq_makefile.cmx:
tools/coq-tex.cmo:
tools/coq-tex.cmx:
coq_fix_code.o: kernel/byterun/coq_fix_code.c \
- /usr/lib/ocaml/3.09.2/caml/config.h \
- /usr/lib/ocaml/3.09.2/caml/compatibility.h \
- /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
- /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
- /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \
+ /usr/local/lib/ocaml/caml/config.h \
+ /usr/local/lib/ocaml/caml/compatibility.h \
+ /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \
+ /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \
+ /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \
kernel/byterun/coq_fix_code.h
coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
- /usr/lib/ocaml/3.09.2/caml/compatibility.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
- /usr/lib/ocaml/3.09.2/caml/alloc.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
- kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
- /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
- kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
+ /usr/local/lib/ocaml/caml/mlvalues.h \
+ /usr/local/lib/ocaml/caml/compatibility.h \
+ /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+ kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
+ /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
+ kernel/byterun/coq_jumptbl.h
coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
- /usr/lib/ocaml/3.09.2/caml/compatibility.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
- /usr/lib/ocaml/3.09.2/caml/alloc.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \
- kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
- /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \
- kernel/byterun/coq_interp.h
+ /usr/local/lib/ocaml/caml/mlvalues.h \
+ /usr/local/lib/ocaml/caml/compatibility.h \
+ /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
+ kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \
+ /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h
coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h \
- /usr/lib/ocaml/3.09.2/caml/compatibility.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \
+ /usr/local/lib/ocaml/caml/mlvalues.h \
+ /usr/local/lib/ocaml/caml/compatibility.h \
+ /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
- /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \
- /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \
- /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \
- /usr/lib/ocaml/3.09.2/caml/alloc.h
+ /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \
+ /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \
+ /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \
+ /usr/local/lib/ocaml/caml/alloc.h
diff --git a/CHANGES b/CHANGES
index 34e7f506..d1f6efe1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,14 @@
+Changes from V8.1pl1 to V8.1pl2
+===============================
+
+Installation
+
+- Support for compilation with ocaml 3.10 and (transitional) camlp5.
+
+Bug fixes
+
+- Many bugs have been fixed (cf coq-bugs web page)
+
Changes from V8.1 to V8.1pl1
============================
diff --git a/INSTALL b/INSTALL
index 1577ba90..8658fb0e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -5,16 +5,51 @@
WHAT DO YOU NEED ?
==================
- Coq is designed to work on computers equipped with the Unix operating
- system. In order to compile Coq V8.1 you need:
+ Coq is designed to work on computers equipped with a POSIX (Unix or
+ a clone) operating system. It also works under Microsoft Windows
+ (see INSTALL.win); for a precompiled MacOS X package, see
+ INSTALL.macosx.
+
+ Coq is known to be actively used under GNU/Linux (i386, amd64 and
+ ppc) and FreeBSD. Automated tests are run under many, many
+ different architectures under GNU/Linux.
+
+ Naturally, Coq will run faster on an architecture where OCaml can
+ compile to native code, rather than only bytecode. At time of
+ writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64,
+ HPPA and StrongArm. See
+ http://caml.inria.fr/ocaml/portability.en.html for details.
+
+
+ Your OS may already contain Coq under the form of a precompiled
+ package or ready-to-compile port. In this case, and if the supplied
+ version suits you, follow the usual procedure for your OS to
+ install it. E.g.:
+
+ - Debian GNU/Linux (or Debian GNU/k*BSD or ...):
+
+ aptitude install coq
+
+ - Gentoo GNU/Linux: emerge sci-mathematics/coq
+
+
+ Should you need or prefer to compile Coq V8.1 yourself, you need:
- Objective Caml version 3.07 or later
(available at http://caml.inria.fr/)
-
- Until now, it has mainly been tested on Sun workstations running Solaris,
- and DEC alpha and Pentium workstations running Linux. By FTP, Coq
- comes as a single compressed tar-file. You have probably already
- decompressed it if you are reading this document.
+
+ For Ocaml version >= 3.10.0, you also need to install camlp5
+ version <= 4.08, or 5.01 transitional
+ (see http://pauillac.inria.fr/~ddr/camlp5/)
+
+ - GNU Make
+
+ - a C compiler
+
+ - for Coqide, the Lablgtk development files, and the GTK libraries
+
+ By FTP, Coq comes as a single compressed tar-file. You have
+ probably already decompressed it if you are reading this document.
QUICK INSTALLATION PROCEDURE.
diff --git a/INSTALL.ide b/INSTALL.ide
index 0ca3d9e0..365f59ee 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -8,24 +8,66 @@ DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you
loose a proof, you may encounter unexpected bugs.
Do not hesitate to send suggestions/bug reports.
+DISTRIBUTION PACKAGES
+
+Your POSIX operating system may already contain precompiled packages
+for Coq, including CoqIde, or a ready-to-compile... If the version
+provided there suits you, follow the usual procedure for your
+operating system.
+
+E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do:
+ aptitude install coqide
+On Gentoo GNU/Linux, do:
+ USE=ide emerge sci-mathematics/coq
+
+Else, read the rest of this document to compile your own CoqIde.
+
REQUIREMENT:
- OCaml >= 3.07 with native thread support.
- make world must succeed.
- The graphical toolkit Gtk 2.x. See http://www.gtk.org.
- The official supported version is at least 2.2.x.
- You may still compile CoqIde with older 2.0.x versions and
+ The official supported version is at least 2.8.x.
+ You may still compile CoqIde with older versions and
use all features.
Run
"pkg-config --modversion gtk+-2.0"
to check your version.
- All recent distributions have precompiled packages.
- Do not forget to install the developement headers packages.
- As for Debian/woody,
+ All recent distributions have precompiled packages.
+ Do not forget to install the development headers packages.
+ As for Debian or Ubuntu,
apt-get install libgtk2.0-dev
- should be enough.
+ should be enough.
+
+ - The OCaml bindings for for GTK+ 2.x, lablgtk2.
+
+ Your distribution may contain precompiled packages. For
+ example, for Debian, run
+ aptitude install liblablgtk2-ocaml-dev
+
+ If it does not, see
+ http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html .
+
+ The latest official release of lablftk2 is here:
+ http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz
+
+ Note that even if its README requires ocaml > 3.07, it works
+ ok with 3.07. If you are in a hurry just run :
+
+ cd /tmp && \
+ wget \
+ http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz && \
+ tar zxvf lablgtk-2.10.0.tar.gz && \
+ cd lablgtk-2.10.0 && \
+ ./configure && \
+ make world && \
+ make install
+
+ You must have write access to the OCaml standard library path.
+
+ If this fails, read lablgtk-2.10.0/README.
INSTALLATION
- 0) For optimal performance, OCaml must support native threads (aka pthreads).
+0) For optimal performance, OCaml must support native threads (aka pthreads).
If this not the case, this means that Coq computations will be slow and
"make ide" will fail. Use "make bin/coqide.byte" instead. To fix this
problem, just recompile OCaml from source and configure OCaml with :
@@ -33,26 +75,7 @@ INSTALLATION
In case you install over an existing copy of OCaml, you should better
empty the OCaml installation directory.
- 1) You need to install the OCaml stub library lablgtk2. See
- http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
- The first official release of lablftk2 is here:
- http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz
- Note that even if its README requires ocaml > 3.07, it works ok with 3.07.
- If you are in a hurry just run :
-
-cd /tmp && \
-wget \
- http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz && \
-tar zxvf lablgtk-2.2.0.tar.gz && \
-cd lablgtk-2.2.0 && \
-./configure && \
-make world && \
-make install
-
- You must have write access to the OCaml standard library path.
- If this fails read lablgtk-2.2.0/README.
-
-2) Go into your Coq source directory and, as usual, configure with:
+1) Go into your Coq source directory and, as usual, configure with:
./configure
@@ -68,7 +91,7 @@ make install
In case you are upgrading from an old version you may need to run
make clean-ide
-3) You may now run bin/coqide
+2) You may now run bin/coqide
NOTES
diff --git a/INSTALL.win b/INSTALL.win
deleted file mode 100644
index f2cddb8a..00000000
--- a/INSTALL.win
+++ /dev/null
@@ -1,63 +0,0 @@
-*****************************************************************
-* INSTALLATION PROCEDURE FOR THE COQ V8 SYSTEM UNDER WINDOWS OS *
-*****************************************************************
-
- The binary distribution consists in a .zip archive file. This .zip contains
-long filenames and cannot therefore be unpacked with pkunzip version 2. Use
-either Winzip (shareware) or the Windows version of unzip (freeware):
-
- http://www.winzip.com/
- http://www.winimage.com/zLibDll/
-
- Unzipping the distribution creates (among others) the following directories
-and files:
-
- coq\bin\ The command-line tools
- coq\lib\ The standard library files
- coq\emacs A Coq mode for your Emacs
- coq\man\man1 The man pages for the command-line tools
-
- There are two cases to consider :
-
-1. You unzip in the root of your drive (say C):
-===============================================
-
- Hence Coq will be installed in C:\coq
-
- You must add the C:\coq\bin path to your environment variable PATH. This is
-done by adding the following line to your AUTOEXEC.BAT:
-
- set PATH=%PATH%;C:\coq\bin
-
- You may also want to specify where Coq has to look for your configuration
-file .coqrc (not mandatory), e.g.:
-
- set HOME=C:\My_Documents\Coq
-
-2. You unzip in some other place (say D:\My_Dir):
-=================================================
-
- You must add the D:\My_Dir\coq\bin path to your environment variable PATH.
-This is done by adding the following line to AUTOEXEC.BAT:
-
- set PATH=%PATH%;D:\My_Dir\coq\bin
-
- You must also set the environment variables COQBIN and COQLIB to tell Coq
-that binaries and libraries are not in the default place. This is done by
-adding the following lines to your AUTOEXEC.BAT:
-
- set COQBIN=D:\My_Dir\coq\bin
- set COQLIB=D:\My_Dir\coq\lib
-
- You may also want to specify where Coq has to look for your configuration
-file .coqrc (not mandatory), e.g.:
-
- set HOME=C:\My_Documents\Coq
-
-PROBLEMS:
-=========
-
- If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
-
- The Coq Team.
diff --git a/Makefile b/Makefile
index 64cc07a2..b27acbb4 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 10014 2007-07-17 15:14:39Z notin $
+# $Id: Makefile 10216 2007-10-11 13:44:00Z notin $
# Makefile for Coq
@@ -79,18 +79,19 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
-I contrib/field -I contrib/subtac -I contrib/rtauto \
-I contrib/recdef
-MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) $(COQIDEINCLUDES)
OCAMLC += $(CAMLFLAGS)
OCAMLOPT += $(CAMLFLAGS)
BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(INLINEFLAG) $(USERFLAGS)
-DEPFLAGS=$(LOCALINCLUDES)
+DEPFLAGS= -slash $(LOCALINCLUDES)
OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
-CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo
+CAMLP4EXTENSIONS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo pa_macro.cmo
+CAMLP4OPTIONS=$(CAMLP4COMPAT) -D$(CAMLVERSION)
CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)|\1|p'
COQINCLUDES= # coqtop includes itself the needed paths
@@ -352,12 +353,6 @@ OBJSCMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
CINCLUDES= -I $(CAMLHLIB)
-ifeq ($(CAMLVERSION),OCAML307)
- CFLAGS=-fno-defer-pop -Wall -Wno-unused -DOCAML_307
-else
- CFLAGS=-fno-defer-pop -Wall -Wno-unused
-endif
-
# libcoqrun.a
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
@@ -611,7 +606,7 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/config_file.cmo \
ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo
COQIDECMX=$(COQIDECMO:.cmo=.cmx)
-COQIDEFLAGS=-thread -I +lablgtk2
+COQIDEFLAGS=-thread $(COQIDEINCLUDES)
BEFOREDEPEND+= ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
BEFOREDEPEND+= ide/config_parser.mli ide/config_parser.ml
BEFOREDEPEND+= ide/utf8_convert.ml
@@ -1168,7 +1163,7 @@ $(COQDEP): $(COQDEPCMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
-BEFOREDEPEND+= tools/coqdep_lexer.ml $(COQDEP)
+BEFOREDEPEND+= tools/coqdep_lexer.ml
GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo
@@ -1262,6 +1257,7 @@ install-tools::
$(MKDIR) $(FULLBINDIR)
# recopie des fichiers de style pour coqide
$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+ touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
cp $(TOOLS) $(FULLBINDIR)
@@ -1483,7 +1479,7 @@ dev/printers.cma: $(PRINTERSCMO)
parsing/grammar.cma: $(GRAMMARCMO)
$(SHOW)'Testing $@'
@touch test.ml4
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
@@ -1500,15 +1496,15 @@ ML4FILES +=parsing/g_minicoq.ml4 \
parsing/g_decl_mode.ml4
-# BEFOREDEPEND+= $(GRAMMARCMO)
+BEFOREDEPEND+= $(GRAMMARCMO)
# BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml
-# File using pa_ifdef and only necessary for parsing ml files
+# File using pa_macro and only necessary for parsing ml files
parsing/q_coqast.cmo: parsing/q_coqast.ml4
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $<
# toplevel/mltop.ml4 (ifdef Byte)
@@ -1522,11 +1518,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml
toplevel/mltop.byteml: toplevel/mltop.ml4
$(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@
+ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo -DByte -impl $< > $@ || rm -f $@
toplevel/mltop.optml: toplevel/mltop.ml4
$(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@
+ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo -impl $< > $@ || rm -f $@
ML4FILES += toplevel/mltop.ml4
@@ -1571,11 +1567,11 @@ ML4FILES += lib/pp.ml4 lib/compat.ml4
lib/compat.cmo: lib/compat.ml4
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $<
lib/compat.cmx: lib/compat.ml4
$(SHOW)'OCAMLOPT $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $<
# files compiled with camlp4 because of streams syntax
@@ -1591,11 +1587,11 @@ ML4FILES += contrib/xml/xml.ml4 \
parsing/lexer.cmx: parsing/lexer.ml4
$(SHOW)'OCAMLOPT4 $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $<
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $<
parsing/lexer.cmo: parsing/lexer.ml4
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $<
# pretty printing of the revision number when compiling a checked out
# source tree
@@ -1647,17 +1643,11 @@ archclean::
.ml4.cmx:
$(SHOW)'OCAMLOPT4 $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $<
.ml4.cmo:
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
-
-%.ml: %.ml4
- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
-
-#.v.vo:
-# $(BOOTCOQTOP) -compile $*
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $<
.el.elc:
echo "(setq load-path (cons \".\" load-path))" > $*.compile
@@ -1721,8 +1711,8 @@ cleanconfig::
alldepend: depend dependcoq
-dependcoq:
- $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \
+dependcoq: $(BEFOREDEPEND) $(COQDEP)
+ $(COQDEP) -slash -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \
$(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq
# Build dependencies ignoring failures in building ml files from ml4 files
@@ -1745,30 +1735,43 @@ ML4FILESML = $(ML4FILES:.ml4=.ml)
# Expresses dependencies of the .ml4 files w.r.t their grammars
.PHONY: dependp4
-dependp4: $(ML4FILES)
+dependp4:
rm -f .depend.camlp4
for f in $(ML4FILES); do \
printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \
echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \
done
+# Produce the .ml files using Makefile.dep
+.PHONY: ml4filesml
+ml4filesml:: .depend.camlp4 parsing/grammar.cma
+ $(MAKE) -f Makefile.dep $(ML4FILESML)
+
+
.PHONY: depend
-depend: $(BEFOREDEPEND) dependp4 $(ML4FILESML)
+depend: dependp4 ml4filesml $(BEFOREDEPEND)
# 1. We express dependencies of the .ml files w.r.t their grammars
# 2. Then we are able to produce the .ml files using Makefile.dep
# 3. We compute the dependencies inside the .ml files using ocamldep
$(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend
# 4. We express dependencies of .cmo and .cmx files w.r.t their grammars
for f in $(ML4FILES); do \
- printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \
- echo `$(CAMLP4DEPS) $$f` >> .depend; \
- printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \
- echo `$(CAMLP4DEPS) $$f` >> .depend; \
+ bn=`dirname $$f`/`basename $$f .ml4`; \
+ deps=`$(CAMLP4DEPS) $$f`; \
+ if [[ $${deps} != "" ]]; then \
+ /bin/mv -f .depend .depend.tmp; \
+ sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \
+ -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \
+ .depend.tmp > .depend; \
+ /bin/rm -f .depend.tmp; \
+ fi; \
done
# 5. We express dependencies of .o files
- $(CC) -I $(CAMLHLIB) -MM kernel/byterun/*.c >> .depend
+ $(CC) -MM -isystem $(CAMLHLIB) kernel/byterun/*.c >> .depend
# 6. Finally, we erase the generated .ml files
rm -f $(ML4FILESML)
+# and the .cmo and .cmi files needed by grammar.cma
+ rm -f rm parsing/*.cm[io] lib/pp.cm[io] lib/compat.cm[io]
# 7. Since .depend contains correct dependencies .depend.devel can be deleted
# (see dev/Makefile.dir for details about this file)
if [ -e makefile ]; then >.depend.devel; else rm -f .depend.devel; fi
@@ -1787,7 +1790,6 @@ devel:
-include .depend
-include .depend.coq
--include .depend.camlp4
clean::
find . -name "\.#*" -exec rm -f {} \;
diff --git a/Makefile.dep b/Makefile.dep
index 93ca6dfa..8569dfbf 100644
--- a/Makefile.dep
+++ b/Makefile.dep
@@ -12,4 +12,4 @@ include Makefile
include .depend.camlp4
.ml4.ml:
- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+ $(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
diff --git a/PROBLEMES b/PROBLEMES
new file mode 100644
index 00000000..4e522a8a
--- /dev/null
+++ b/PROBLEMES
@@ -0,0 +1,54 @@
+Intuition plante en 7.1 à certains endroits où il réussissait en 6.3.
+Y a-t-il une explication ? (cf contrib sheaves de Chicli - HH)
+
+----------------------------------------------------------------------
+Theorem toto : (A:Prop)A->A.
+Refine [A;x]?.
+produit le message "type_of: this is not a well-typed term. Please report."
+
+----------------------------------------------------------------------
+"Intro until 1" plante avec le message
+"Error: Internal tactic intro cannot be applied to intro until #GENTERM 1"
+--> intro est répété + GENTERM
+
+----------------------------------------------------------------------
+La synthèse du ? dans l'exemple suivant se fait en V6 mais pas en V7:
+
+Inductive Prod : Type := Pair : Set->Set->Prod.
+Definition Pfst := [p:Prod](let (x, _) = p in x).
+Variable P : Prod->Type.
+Variable i : Set->(P (Pair nat nat)).
+Variable j : (X:Prod)(Pfst X)->(P X)->Prop.
+Variable k : nat.
+Variable l : (P (Pair nat nat)).
+Check (!j ? k (i nat)). (* Marche en V6, pas en V7 *)
+Check (!j ? k l). (* Ne marche ni en V6 !!! ni en V7 *)
+
+----------------------------------------------------------------------
+Des CASTEDCOMMAND s'affiche dans les scripts de preuves.
+
+----------------------------------------------------------------------
+Probleme d'affichage des scripts de preuve (disparition des THEN)
+Compute affiche Cbv Beta Iota
+
+----------------------------------------------------------------------
+Variable + Record => clash. Exemple:
+
+Section S.
+Variable F:Set.
+Record R [ F:Set; x:F ] : Set := { c : x=x }.
+ => Error: new_isevar_sign: two vars have the same name
+
+----------------------------------------------------------------------
+Declaration de Local a l'interieur d'un but ...
+
+----------------------------------------------------------------------
+Certains Clear deviennent impossible car la variable apparait dans
+un lemme local, c'est plutot sain ...
+
+----------------------------------------------------------------------
+l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les
+binding je pense) d'ou des erreurs de syntaxe ... pure_numarg est
+plus sûr
+REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la
+syntaxe, elle est incompatible avec L_tac.
diff --git a/README.win b/README.win
index 4ba9ac1b..0f8023bb 100644
--- a/README.win
+++ b/README.win
@@ -6,7 +6,12 @@ THE COQ V8.1 SYSTEM
INSTALLATION.
=============
- See the file INSTALL.win for installation procedure.
+ The Coq package for Windows comes with an auto-installer. It will
+install Coq binaries and libraries under any directory you specify
+(C:\Program Files\Coq is the default path). It also creates shortcuts
+in the Windows menus. Alternatively, you can launch Coq using Coq.bat
+and Coqide.bat in the installation directory (C:\Program Files\Coq by
+default).
COMPILATION.
============
@@ -15,25 +20,34 @@ COMPILATION.
distribution. If you really need to recompile under Windows, here
are some indications:
- 1- Install ocaml version 3.07 or later, Visual C++ (needed
- for the -custom option of ocaml) and MASM (needed if you want
- to produce a native version).
+ 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3.
+ See: http://caml.inria.fr
- 2- Install a complete set of Unix utilities (used by Makefiles).
- See: http://sources.redhat.com/cygwin/.
+ 2- Install a shell environment with at least:
+ - a C compiler (gcc),
+ - the GNU make utility
- 3- Under cygwin, type successively
+ The Cygwin environment is well suited for compiling Coq
+ (official packages are made using Cygwin) See:
+ http://www.cygwin.com
+
+ 3- In order to compile Coqide, you will need the LablGTK library
+ See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
+
+ You also need to install the GTK libraries for Windows (see the
+ installation instruction for LablGTK)
+
+ 4- In a shell window, type successively
./configure
make world
make install
- make clean
- 4- Though not nescessary, you can find useful:
+ 5- Though not nescessary, you can find useful:
- Windows version of (X)Emacs: it is a powerful environment for
developpers with coloured syntax, modes for compilation and debug,
and many more. It is free. See: http://www.gnu.org/software.
- - Windows cvs client (very useful if you have access to the Coq
+ - Windows subversion client (very useful if you have access to the Coq
archive).
Good luck :-)
diff --git a/TODO b/TODO
new file mode 100644
index 00000000..dc80e4c3
--- /dev/null
+++ b/TODO
@@ -0,0 +1,51 @@
+Langage:
+
+Distribution:
+
+Environnement:
+
+- Porter SearchIsos
+
+Noyau:
+
+Tactic:
+
+- Que contradiction raisonne a isomorphisme pres de False
+
+Vernac:
+
+- Print / Print Proof en fait identiques ; Print ne devrait pas afficher
+ les constantes opaques (devrait afficher qqchose comme <opaque>)
+
+Theories:
+
+- Rendre transparent tous les theoremes prouvant {A}+{B}
+- Faire demarrer PolyList.nth a` l'indice 0
+ Renommer l'actuel nth en nth1 ??
+
+Doc:
+
+- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Documenter le filtrage sur les types inductifs avec let-ins (dont la
+ compatibilite V6)
+
+- Ajouter let dans les règles du CIC
+ -> FAIT, mais reste a documenter le let dans les inductifs
+ et les champs manifestes dans les Record
+- revoir le chapitre sur les tactiques utilisateur
+- faut-il mieux spécifier la sémantique de Simpl (??)
+
+- Préciser la clarification syntaxique de IntroPattern
+- preciser que Goal vient en dernier dans une clause pattern list et
+ qu'il doit apparaitre si il y a un "in"
+
+- Omega Time debranche mais Omega System et Omega Action remarchent ?
+- Ajout "Replace in" (mais TODO)
+- Syntaxe Conditional tac Rewrite marche, à documenter
+- Documenter Dependent Rewrite et CutRewrite ?
+- Ajouter les motifs sous-termes de ltac
+
+- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
+- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
+- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
+--> mettre à jour le CHANGES (vers la ligne 72)
diff --git a/config/Makefile.template b/config/Makefile.template
index 3ea7c7c9..1e611356 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -31,7 +31,7 @@ EMACSLIB="EMACSLIBDIRECTORY"
EMACS=EMACSCOMMAND
# Path to Coq distribution
-COQTOP=COQTOPDIRECTORY
+COQSRC=COQSRCDIRECTORY
VERSION=COQVERSION
# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
@@ -48,6 +48,9 @@ CAMLP4O=CAMLP4TOOL
CAMLP4COMPAT=CAMLP4COMPATFLAGS
MYCAMLP4LIB="CAMLP4LIBDIRECTORY"
+# LablGTK
+COQIDEINCLUDES=LABLGTKINCLUDES
+
# Objective-Caml compile command
OCAMLC="BYTECAMLC"
OCAMLOPT="NATIVECAMLC"
@@ -62,7 +65,7 @@ CAMLOPTLINK="NATIVECAMLC"
CAMLMKTOP="CAMLMKTOPEXEC"
# Caml flags
-CAMLFLAGS=CAMLANNOTATEFLAG
+CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
# Compilation debug flag
CAMLDEBUG=COQDEBUGFLAG
@@ -73,16 +76,15 @@ INLINEFLAG=COQINLINEFLAG
# User compilation flag
USERFLAGS=
+# Flags for GCC
+CFLAGS=CCOMPILEFLAGS
+
# Compilation profile flag
CAMLTIMEPROF=COQPROFILEFLAG
# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
BEST=BESTCOMPILER
-# For Camlp4 use
-P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
-P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
-
# Your architecture
# Can be obtain by UNIX command arch
ARCH=ARCHITECTURE
diff --git a/config/coq_config.mli b/config/coq_config.mli
index c214344e..bf77f0f3 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coq_config.mli 9115 2006-09-01 13:47:00Z notin $ i*)
+(*i $Id: coq_config.mli 10185 2007-10-06 18:05:13Z herbelin $ i*)
val local : bool (* local use (no installation) *)
@@ -18,6 +18,7 @@ val coqtop : string (* where are the sources *)
val camldir : string (* base directory of OCaml binaries *)
val camllib : string (* for Dynlink *)
+val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *)
val camlp4lib : string (* where is the library of Camlp4 *)
val best : string (* byte/opt *)
diff --git a/configure b/configure
index c0cd3775..e964539a 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
#
##################################
-VERSION=8.1pl1
-DATE="Jul. 2007"
+VERSION=8.1pl2
+DATE="Oct. 2007"
# a local which command for sh
which () {
@@ -42,7 +42,11 @@ usage () {
echo "-coqdocdir"
echo -e "\tSpecifies where Coqdoc style files are to be installed\n"
echo "-camldir"
- echo -e "\tTells configure where to look for OCaml files\n"
+ echo -e "\tSpecifies the path to the OCaml library\n"
+ echo "-lablgtkdir"
+ echo -e "\tSpecifies the path to the Lablgtk library\n"
+ echo "-camlp5dir"
+ echo -e "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
echo "-arch"
echo -e "\tSpecifies the architecture\n"
echo "-opt"
@@ -86,6 +90,7 @@ coq_profile_flag=
coq_annotate_flag=
coq_inline_flag=
best_compiler=opt
+cflags="-fno-defer-pop -Wall -Wno-unused"
gcc_exec=gcc
ar_exec=ar
@@ -100,6 +105,7 @@ mandir_spec=no
emacslib_spec=no
emacs_spec=no
camldir_spec=no
+lablgtkdir_spec=no
coqdocdir_spec=no
fsets_opt=no
fsets=all
@@ -109,7 +115,6 @@ arch_spec=no
coqide_spec=no
with_geoproof=false
-# COQTOP=`pwd`
COQSRC=`pwd`
# Parse command-line arguments
@@ -126,7 +131,7 @@ while : ; do
reals_opt=yes
reals=all;;
-src|--src) src_spec=yes
- COQTOP="$2"
+ COQSRC="$2"
shift;;
-bindir|--bindir) bindir_spec=yes
bindir="$2"
@@ -149,6 +154,12 @@ while : ; do
-camldir|--camldir) camldir_spec=yes
camldir="$2"
shift;;
+ -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
+ lablgtkdir="$2"
+ shift;;
+ -camlp5dir|--camlp5dir)
+ camlp5dir="$2"
+ shift;;
-arch|--arch) arch_spec=yes
arch=$2
shift;;
@@ -229,6 +240,8 @@ case $arch_spec in
# cygwin returns a name of the form /cygdrive/c/...
# that coqc does not understand; need to transform it
COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"`
+ elif test -x /bin/uname ; then
+ ARCH=`/bin/uname -s`
elif test -x /usr/bin/uname ; then
ARCH=`/usr/bin/uname -s`
else
@@ -274,7 +287,7 @@ fi
case $camldir_spec in
no) CAMLC=`which $bytecamlc`
case "$CAMLC" in
- "") echo "$bytecamlc is not present in your path !"
+ "") echo "$bytecamlc is not present in your path!"
echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
read CAMLC
@@ -306,6 +319,11 @@ if test ! -f "$CAMLC" ; then
exit 1
fi
+# Under Windows, OCaml only understands Windows filenames (C:\...)
+case $ARCH in
+ win32) CAMLBIN=`cygpath -w ${CAMLBIN}`;;
+esac
+
# this fixes a camlp4 bug under FreeBSD
# ("native-code program cannot do a dynamic load")
if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
@@ -313,24 +331,28 @@ if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
case $CAMLVERSION in
- 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0)
+ 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.08.0)
echo "Your version of Objective-Caml is $CAMLVERSION."
if [ "$CAMLVERSION" = "3.08.0" ] ; then
- echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!"
+ echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!"
else
- echo "You need Objective-Caml 3.06 or later!"
+ echo "You need Objective-Caml 3.07 or later!"
fi
echo "Configuration script failed!"
exit 1;;
- 3.06|3.07*|3.08*)
- echo "You have Objective-Caml $CAMLVERSION. Good!"
- coq_inline_flag="-inline 0";;
+ 3.07*)
+ cflags="$cflags -DOCAML_307"
+ coq_inline_flag="-inline 0"
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
+ 3.08*)
+ coq_inline_flag="-inline 0"
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
?*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
echo "I found the Objective-Caml compiler but cannot find its version number!"
- echo "Is it installed properly ?"
+ echo "Is it installed properly?"
echo "Configuration script failed!"
exit 1;;
esac
@@ -342,11 +364,19 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
if [ "$best_compiler" = "opt" ] ; then
if test -e `which "$nativecamlc"` ; then
CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
- if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
- echo "native and bytecode compilers do not have the same version!"; fi
+ if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
+ case $CAMLOPTVERSION in
+ 3.09.3|3.1?*) ;;
+ *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
+ best_compiler=byte
+ echo "only the bytecode version of Coq will be available."
+ esac
+ elif [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
+ echo "Native and bytecode compilers do not have the same version!";
+ fi
echo "You have native-code compilation. Good!"
else
- best_compiler=byte ;
+ best_compiler=byte
echo "You have only bytecode compilation."
fi
fi
@@ -354,19 +384,54 @@ fi
# For coqmktop & bytecode compiler
-CAMLLIB=`"$CAMLC" -where`
+case $ARCH in
+ win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
+ CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
+ *)
+ CAMLLIB=`"$CAMLC" -where`
+ esac
+
+
+# Camlp4 / Camlp5 configuration
+# Very basic for the moment: if camlp5 exists, we use it...
+
+if [ "$camlp5dir" != "" ]; then
+ CAMLP4=camlp5
+ CAMLP4LIB=$camlp5dir
+ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+elif [ "$CAMLTAG" = "OCAML310" ]; then
+ if [ -x "${CAMLLIB}/camlp5" ]; then
+ CAMLP4LIB=+camlp5
+ elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
+ CAMLP4LIB=+site-lib/camlp5
+ else
+ echo "Objective Caml 3.10 found but no Camlp5 installed."
+ echo "Configuration script failed!"
+ exit 1
+ fi
+ CAMLP4=camlp5
+ camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+else
+ CAMLP4=camlp4
+ CAMLP4LIB=+camlp4
+fi
+
+if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
+ echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK."
+ echo "Configuration script failed!"
+ exit 1
+fi
+
-# Camlp4 (greatly simplified since merged with ocaml)
+case $CAMLP4LIB in
+ +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
+ *) FULLCAMLP4LIB=$CAMLP4LIB;;
+esac
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day)
CAMLP4BIN=${CAMLBIN}
-#case $OS in
-# Win32)
- CAMLP4LIB=+camlp4
-# ;;
-# *)
-# CAMLP4LIB=${CAMLLIB}/camlp4
-#esac
# OS dependent libraries
@@ -380,7 +445,8 @@ case $ARCH in
esac;;
alpha) OSDEPLIBS="-cclib -lunix";;
win32) OS="Win32"
- OSDEPLIBS="-cclib -lunix";;
+ OSDEPLIBS="-cclib -lunix"
+ cflags="-mno-cygwin $cflags";;
*) OSDEPLIBS="-cclib -lunix"
esac
@@ -396,24 +462,50 @@ fi
# Which coqide is asked ? which one is possible ?
if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
- echo "CoqIde disabled as requested"
-elif [ ! -x "${CAMLLIB}/lablgtk2" ]; then
- echo "LablGtk2 not found: CoqIde will not be available"
- COQIDE=no
-elif [ -z "`grep -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli`" ]; then
- echo "LablGtk2 found but too old: CoqIde will not be available"
- COQIDE=no;
-elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
- echo "LablGtk2 found, bytecode CoqIde will be used as requested"
- COQIDE=byte
-elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
- echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
- COQIDE=byte
-else
- echo "LablGtk2 found, native threads: native CoqIde will be available"
- COQIDE=opt
+ echo "CoqIde disabled as requested."
+else
+ case $lablgtkdir_spec in
+ no)
+ if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
+ lablgtkdir=${CAMLLIB}/lablgtk2
+ elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
+ lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
+ fi;;
+ yes)
+ if [ ! -f "$lablgtkdir/glib.mli" ]; then
+ echo "Incorrect LablGtk2 library (glib.mli not found)."
+ echo "Configuration script failed!"
+ exit 1
+ fi;;
+ esac
+ if [ "$lablgtkdir" = "" ]; then
+ echo "LablGtk2 not found: CoqIde will not be available."
+ COQIDE=no
+ elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
+ echo "LablGtk2 found but too old: CoqIde will not be available."
+ COQIDE=no;
+ elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
+ echo "LablGtk2 found, bytecode CoqIde will be used as requested."
+ COQIDE=byte
+ elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
+ echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
+ COQIDE=byte
+ else
+ echo "LablGtk2 found, native threads: native CoqIde will be available."
+ COQIDE=opt
+ fi
fi
+case $COQIDE in
+ byte|opt)
+ case $lablgtkdir_spec in
+ no) LABLGTKLIB=+lablgtk2 # Pour le message
+ LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
+ yes) LABLGTKLIB="$lablgtkdir" # Pour le message
+ LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
+ esac;;
+ no) LABLGTKINCLUDES="";;
+esac
# Tell on windows if ocaml understands cygwin or windows path formats
@@ -442,14 +534,13 @@ esac
###########################################
# bindir, libdir, mandir, etc.
-canonical_pwd () {
-ocaml 2>&1 1>/dev/null <<EOF
- prerr_endline(Sys.getcwd());;
-EOF
-}
-
case $src_spec in
- no) COQTOP=`canonical_pwd`
+ no) COQTOP=${COQSRC}
+esac
+
+# OCaml only understand Windows filenames (C:\...)
+case $ARCH in
+ win32) COQTOP=`cygpath -w ${COQTOP}`
esac
case $ARCH in
@@ -578,6 +669,9 @@ echo " Objective-Caml/Camlp4 version : $CAMLVERSION"
echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN"
echo " Objective-Caml library in : $CAMLLIB"
echo " Camlp4 library in : $CAMLP4LIB"
+if test "$COQIDE" != "no"; then
+echo " Lablgtk2 library in : $LABLGTKLIB"
+fi
if test "$fsets" = "all"; then
echo " FSets theory : All"
else
@@ -609,13 +703,35 @@ escape_var () {
EOF
}
-export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB
-ESCCOQTOP="`VAR=COQTOP escape_var`"
-ESCBINDIR="`VAR=BINDIR escape_var`"
-ESCLIBDIR="`VAR=LIBDIR escape_var`"
-ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
-ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
+# damned backslashes under M$Windows
+case $ARCH in
+ win32)
+ ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
+ ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
+ ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
+ ;;
+ *)
+ ESCCOQTOP="$COQTOP"
+ ESCBINDIR="$BINDIR"
+ ESCLIBDIR="$LIBDIR"
+ ESCCAMLDIR="$CAMLBIN"
+ ESCCAMLLIB="$CAMLLIB"
+ ESCMANDIR="$MANDIR"
+ ESCEMACSLIB="$EMACSLIB"
+ ESCCOQDOCDIR="$COQDOCDIR"
+ ESCCAMLP4BIN="$CAMLP4BIN"
+ ESCCAMLP4LIB="$CAMLP4LIB"
+ ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
+ ;;
+esac
mlconfig_file="$COQSRC/config/coq_config.ml"
rm -f $mlconfig_file
@@ -628,6 +744,7 @@ let coqlib = "$ESCLIBDIR"
let coqtop = "$ESCCOQTOP"
let camldir = "$ESCCAMLDIR"
let camllib = "$ESCCAMLLIB"
+let camlp4 = "$CAMLP4"
let camlp4lib = "$ESCCAMLP4LIB"
let best = "$best_compiler"
let arch = "$ARCH"
@@ -666,29 +783,8 @@ chmod a-w "$mlconfig_file"
rm -f "$COQSRC/config/Makefile"
-# damned backslashes under M$Windows (bis)
-case $ARCH in
- win32)
- ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
- ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
- ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
- ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
- ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
- ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
- ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
- ;;
- *)
- ESCCOQTOP="$COQTOP"
- ESCBINDIR="$BINDIR"
- ESCLIBDIR="$LIBDIR"
- ESCMANDIR="$MANDIR"
- ESCEMACSLIB="$EMACSLIB"
- ESCCOQDOCDIR="$COQDOCDIR"
- ESCCAMLP4BIN="$CAMLP4BIN" ;;
-esac
-
sed -e "s|LOCALINSTALLATION|$local|" \
- -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \
+ -e "s|COQSRCDIRECTORY|$COQSRC|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
@@ -706,10 +802,12 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-e "s|CAMLP4TOOL|$camlp4oexec|" \
-e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
+ -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
-e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-e "s|COQINLINEFLAG|$coq_inline_flag|" \
-e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
+ -e "s|CCOMPILEFLAGS|$cflags|" \
-e "s|BESTCOMPILER|$best_compiler|" \
-e "s|EXECUTEEXTENSION|$EXE|" \
-e "s|BYTECAMLC|$bytecamlc|" \
@@ -735,19 +833,14 @@ chmod a-w "$COQSRC/config/Makefile"
# Building the $COQTOP/dev/ocamldebug-coq file
##################################################
-OCAMLDEBUGCOQ=$COQTOP/dev/ocamldebug-coq
+OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
if test "$coq_debug_flag" = "-g" ; then
rm -f $OCAMLDEBUGCOQ
- if [ "$CAMLP4LIB" = "+camlp4" ] ; then
- CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
- else
- CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
- fi
sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-e "s|COQLIBDIRECTORY|$LIBDIR|" \
-e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
- -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \
+ -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
$OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
chmod a-w,a+x $OCAMLDEBUGCOQ
fi
@@ -757,7 +850,7 @@ fi
####################################################
if [ ! "$COQIDE" = "no" ]; then
- if grep "class view " "$CAMLLIB/lablgtk2/gText.mli" | grep -q "\[>" ; then
+ if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
else
cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
@@ -773,4 +866,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 10039 2007-07-20 22:04:33Z notin $
+# $Id: configure 10215 2007-10-11 13:13:51Z herbelin $
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 86251254..dc0dec0e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -199,7 +199,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
let ind=destInd h in
let types=Inductiveops.arities_of_constructors env ind in
let lp=Array.length types in
- let ci=(snd cstr)-1 in
+ let ci=pred (snd cstr) in
let branch i=
let ti=Term.prod_appvect types.(i) argv in
let rc=fst (Sign.decompose_prod_assum ti) in
@@ -247,7 +247,7 @@ let rec proof_tac p gls =
and tx2=constr_of_term p2.p_rhs in
let typf = pf_type_of gls tf1 in
let typx = pf_type_of gls tx1 in
- let typfx = prod_applist typf [tx1] in
+ let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
let id = pf_get_new_id (id_of_string "f") gls in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 97fa4d77..ffc4b9c4 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -6,11 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *)
open Term
open Proof_type
+val proof_tac: Ccproof.proof -> Proof_type.tactic
+
val cc_tactic : int -> constr list -> tactic
val cc_fail : tactic
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e31b701c..825b3554 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*)
+(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Term
open Declarations
@@ -92,7 +92,8 @@ module Visit : VISIT = struct
let needed_kn kn = KNset.mem kn v.kn
let needed_con c = Cset.mem c v.con
let needed_mp mp = MPset.mem mp v.mp
- let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
+ let add_mp mp =
+ check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
let add_ref = function
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6fd4a3cc..6982ffc6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*)
+(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*)
(*i*)
open Util
@@ -31,10 +31,6 @@ open Mlutil
exception I of inductive_info
-(* A set of all inductive currently being computed,
- to avoid loops in [extract_inductive] *)
-let internal_call = ref KNset.empty
-
(* A set of all fixpoint functions currently being extracted *)
let current_fixpoints = ref ([] : constant list)
@@ -303,13 +299,15 @@ and extract_type_scheme env db c p =
(*S Extraction of an inductive type. *)
and extract_ind env kn = (* kn is supposed to be in long form *)
- try
- if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *)
- else if visible_kn kn then lookup_ind kn (* Standard situation. *)
- else raise Not_found (* Never trust the table for a internal kn. *)
+ let mib = Environ.lookup_mind kn env in
+ try
+ (* For a same kn, we can get various bodies due to module substitutions.
+ We hence check that the mib has not changed from recording
+ time to retrieving time. Ideally we should also check the env. *)
+ let (mib0,ml_ind) = lookup_ind kn in
+ if not (mib = mib0) then raise Not_found;
+ ml_ind
with Not_found ->
- internal_call := KNset.add kn !internal_call;
- let mib = Environ.lookup_mind kn env in
(* First, if this inductive is aliased via a Module, *)
(* we process the original inductive. *)
option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
@@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ip_types = t })
mib.mind_packets
in
- add_ind kn
+ add_ind kn mib
{ind_info = Standard;
ind_nparams = npar;
ind_packets = packets;
@@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ind_packets = packets;
ind_equiv = mib.mind_equiv}
in
- add_ind kn i;
- internal_call := KNset.remove kn !internal_call;
+ add_ind kn mib i;
i
(*s [extract_type_cons] extracts the type of an inductive
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b1a3cb31..6d39faee 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Names
open Term
@@ -60,7 +60,6 @@ let at_toplevel mp =
let visible_kn kn = at_toplevel (base_mp (modpath kn))
let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
(*S The main tables: constants, inductives, records, ... *)
(*s Constants tables. *)
@@ -77,9 +76,9 @@ let lookup_type kn = Cmap.find kn !types
(*s Inductives table. *)
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
let init_inductives () = inductives := KNmap.empty
-let add_ind kn m = inductives := KNmap.add kn m !inductives
+let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
@@ -124,11 +123,24 @@ let reset_tables () =
let id_of_global = function
| ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
- | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
- | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
+ | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+ | ConstructRef ((kn,i),j) ->
+ (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
| _ -> assert false
-let pr_global r = pr_id (id_of_global r)
+let pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (id_of_global r)
+
+(* idem, but with qualification, and only for constants. *)
+
+let pr_long_global r =
+ try Printer.pr_global r
+ with _ -> match r with
+ | ConstRef kn ->
+ let mp,_,l = repr_con kn in
+ str ((string_of_mp mp)^"."^(string_of_label l))
+ | _ -> assert false
(*S Warning and Error messages. *)
@@ -150,13 +162,13 @@ let warning_log_ax r =
spc () ++ str "may lead to incorrect or non-terminating ML terms.")
let check_inside_module () =
- try
- ignore (Lib.what_is_opened ());
- Options.if_verbose warning
- ("Extraction inside an opened module is experimental.\n"^
- "In case of problem, close it first.\n");
- Pp.flush_all ()
- with Not_found -> ()
+ if Lib.is_modtype () then
+ err (str "You can't do that within a Module Type." ++ fnl () ++
+ str "Close it and try again.")
+ else if Lib.is_module () then
+ msg_warning
+ (str "Extraction inside an opened module is experimental.\n" ++
+ str "In case of problem, close it first.\n")
let check_inside_section () =
if Lib.sections_are_opened () then
@@ -164,10 +176,10 @@ let check_inside_section () =
str "Close it and try again.")
let error_constant r =
- err (Printer.pr_global r ++ str " is not a constant.")
+ err (pr_global r ++ str " is not a constant.")
let error_inductive r =
- err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+ err (pr_global r ++ spc () ++ str "is not an inductive type.")
let error_nb_cons () =
err (str "Not the right number of constructors.")
@@ -187,23 +199,23 @@ let error_scheme () =
err (str "No Scheme modular extraction available yet.")
let error_not_visible r =
- err (Printer.pr_global r ++ str " is not directly visible.\n" ++
+ err (pr_global r ++ str " is not directly visible.\n" ++
str "For example, it may be inside an applied functor." ++
str "Use Recursive Extraction to get the whole environment.")
-let error_unqualified_name s1 s2 =
- err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
- "in ML from another name sharing the same basename.\n" ^
- "Please do some renaming.\n"))
-
let error_MPfile_as_mod d =
err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
"Extraction cannot currently deal with this situation.\n"))
let error_record r =
- err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+ err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
str "To help extraction, please use an explicit name.")
+let check_loaded_modfile mp = match base_mp mp with
+ | MPfile dp -> if not (Library.library_is_loaded dp) then
+ err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+ | _ -> ()
+
(*S The Extraction auxiliary commands *)
(*s Extraction AutoInline *)
@@ -310,7 +322,7 @@ let _ = declare_summary "Extraction Lang"
{ freeze_function = (fun () -> !lang_ref);
unfreeze_function = ((:=) lang_ref);
init_function = (fun () -> lang_ref := Ocaml);
- survive_module = false;
+ survive_module = true;
survive_section = true }
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
@@ -342,28 +354,21 @@ let (inline_extraction,_) =
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
export_function = (fun x -> Some x);
classify_function = (fun (_,o) -> Substitute o);
- (*CSC: The following substitution may istantiate a realized parameter.
- The right solution would be to make the substitution erase the
- realizer from the table. However, this is not allowed by Coq.
- In this particular case, though, keeping the realizer is place seems
- to be harmless since the current code looks for a realizer only
- when the constant is a parameter. However, if this behaviour changes
- subtle bugs can happear in the future. *)
subst_function =
- (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))}
+ (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+ }
let _ = declare_summary "Extraction Inline"
{ freeze_function = (fun () -> !inline_table);
unfreeze_function = ((:=) inline_table);
init_function = (fun () -> inline_table := empty_inline_table);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extraction_inline b l =
check_inside_section ();
- check_inside_module ();
let refs = List.map Nametab.global l in
List.iter
(fun r -> match r with
@@ -380,11 +385,11 @@ let print_extraction_inline () =
(str "Extraction Inline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
str "Extraction NoInline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ()))
(* Reset part *)
@@ -423,20 +428,23 @@ let (in_customs,_) =
{(default_object "ML extractions") with
cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
- export_function = (fun x -> Some x)}
+ export_function = (fun x -> Some x);
+ classify_function = (fun (_,o) -> Substitute o);
+ subst_function =
+ (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+ }
let _ = declare_summary "ML extractions"
{ freeze_function = (fun () -> !customs);
unfreeze_function = ((:=) customs);
init_function = (fun () -> customs := Refmap.empty);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extract_constant_inline inline r ids s =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| ConstRef kn ->
@@ -455,7 +463,6 @@ let extract_constant_inline inline r ids s =
let extract_inductive r (s,l) =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| IndRef ((kn,i) as ip) ->
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 66662138..c9a4e8da 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*)
+(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Names
open Libnames
open Miniml
+open Declarations
val id_of_global : global_reference -> identifier
@@ -27,11 +28,11 @@ val error_unknown_module : qualid -> 'a
val error_toplevel : unit -> 'a
val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
-val error_unqualified_name : string -> string -> 'a
val error_MPfile_as_mod : dir_path -> 'a
val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
+val check_loaded_modfile : module_path -> unit
(*s utilities concerning [module_path]. *)
@@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl
val add_type : constant -> ml_schema -> unit
val lookup_type : constant -> ml_schema
-val add_ind : kernel_name -> ml_ind -> unit
-val lookup_ind : kernel_name -> ml_ind
+val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index b55c5443..d8bb9eae 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -152,8 +152,15 @@ Ltac ParseRingComponents lemma :=
(* ring tactics *)
+Ltac relation_carrier req :=
+ let ty := type of req in
+ match eval hnf in ty with
+ ?R -> _ => R
+ | _ => fail 1000 "Equality has no relation type"
+ end.
+
Ltac FV_hypo_tac mkFV req lH :=
- let R := match type of req with ?R -> _ => R end in
+ let R := relation_carrier req in
let FV_hypo_l_tac h :=
match h with @mkhypo (req ?pe _) _ => mkFV pe end in
let FV_hypo_r_tac h :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index f963fc9c..134ba1a8 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
+(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*)
open Pp
open Util
@@ -465,7 +465,8 @@ let op_smorph r add mul req m1 m2 =
let default_ring_equality (r,add,mul,opp,req) =
let is_setoid = function
- {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
+ {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
+ eq_constr req rel (* Qu: use conversion ? *)
| _ -> false in
match default_relation_for_carrier ~filter:is_setoid r with
Leibniz _ ->
@@ -625,6 +626,7 @@ let interp_sign env sign =
(* Same remark on ill-typed terms ... *)
let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
+ check_required_library (cdir@["Ring_base"]);
let env = Global.env() in
let sigma = Evd.empty in
let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
@@ -986,6 +988,7 @@ let default_field_equality r inv req =
inv_m.lem
let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
+ check_required_library (cdir@["Field_tac"]);
let env = Global.env() in
let sigma = Evd.empty in
let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 44680d6d..2d1c6289 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -7,7 +7,11 @@ export COQLIB=COQLIBDIRECTORY
export COQTH=$COQLIB/theories
CAMLBIN=CAMLBINDIRECTORY
OCAMLDEBUG=$CAMLBIN/ocamldebug
-export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+if [ -x "$CAMLBIN/camlp5" ]; then
+ export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
+else
+ export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+fi
exec $OCAMLDEBUG \
-I $CAMLP4LIB \
diff --git a/doc/Makefile b/doc/Makefile
index 403e2047..5158fbeb 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,6 +1,6 @@
# Makefile for the Coq documentation
-# COQTOP needs to be set to a coq source repository
+# COQSRC needs to be set to a coq source repository
# To compile documentation, you need the following tools:
# Dvi: latex (latex2e), bibtex, makeindex
@@ -18,9 +18,9 @@ PDFLATEX=pdflatex
HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea
TEXINPUTS=$(HEVEALIB):.:
-DOCCOQTOP=$(COQTOP)/bin/coqtop
-COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
-COQDOC=$(COQTOP)/bin/coqdoc
+COQTOP=$(COQSRC)/bin/coqtop
+COQTEX=$(COQSRC)/bin/coq-tex -n 72 -image $(COQTOP) -v -sl -small
+COQDOC=$(COQSRC)/bin/coqdoc
#VERSION=POSITIONNEZ-CETTE-VARIABLE
@@ -76,7 +76,7 @@ rectutorial:\
clean:
rm -f */*.dvi */*.aux */*.log */*.bbl */*.blg */*.toc \
*/*.idx */*~ */*.ilg */*.ind */*.dvi.gz */*.ps.gz */*.pdf.gz\
- */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof\
+ */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof \
*/*.hatoc */*.haux */*.hcomind */*.herrind */*.hidx */*.hind \
*/*.htacind */*.htoc */*.v.html
rm -f stdlib/index-list.html stdlib/index-body.html \
@@ -211,7 +211,7 @@ faq/html/index.html: faq/FAQ.v.html
# Standard library
######################################################################
-GLOBDUMP=$(COQTOP)/glob.dump
+GLOBDUMP=$(COQSRC)/glob.dump
LIBDIRS= Logic Bool Arith ZArith QArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
@@ -222,11 +222,11 @@ stdlib/index-body.html: $(GLOBDUMP)
mkdir stdlib/html
(cd stdlib/html;\
$(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
- -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
+ -R $(COQSRC)/theories Coq $(COQSRC)/theories/*/*.v)
mv stdlib/html/index.html stdlib/index-body.html
stdlib/index-list.html: stdlib/index-list.html.template
- COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html
+ COQTOP=$(COQSRC) ./stdlib/make-library-index stdlib/index-list.html
stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html
cat stdlib/index-list.html > $@
@@ -238,8 +238,8 @@ stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/ind
stdlib/Library.coqdoc.tex:
(for dir in $(LIBDIRS) ; do \
$(COQDOC) -q --gallina --body-only --latex --stdout \
- --coqlib_path $(COQTOP) \
- -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done)
+ --coqlib_path $(COQSRC) \
+ -R $(COQSRC)/theories Coq "$(COQSRC)/theories/$$dir/"*.v >> $@ ; done)
stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex
(cd stdlib;\
@@ -282,8 +282,8 @@ install-doc: install-meta install-doc-html install-doc-printable
install-meta:
mkdir $(DOCDIC)
cp LICENCE $(DOCDIC)/LICENCE.doc
-# cp $(COQTOP)/LICENCE $(COQTOP)/CREDITS $(COQTOP)/COPYRIGHT $(DOCDIC)
-# cp $(COQTOP)/README $(COQTOP)/CHANGES $(DOCDIC)
+# cp $(COQSRC)/LICENCE $(COQSRC)/CREDITS $(COQSRC)/COPYRIGHT $(DOCDIC)
+# cp $(COQSRC)/README $(COQSRC)/CHANGES $(DOCDIC)
install-doc-html: all-html
mkdir $(HTMLINSTALLDIR)
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 768d125c..937098b7 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command_windows.ml 9189 2006-09-29 12:39:24Z notin $ *)
+(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *)
class command_window () =
let window = GWindow.window
@@ -69,9 +69,10 @@ object(self)
val notebook = notebook
method window = window
method new_command ?command ?term () =
+ let appendp x = ignore (notebook#append_page x) in
let frame = GBin.frame
~shadow_type:`ETCHED_OUT
- ~packing:notebook#append_page
+ ~packing:appendp
()
in
notebook#goto_page (notebook#page_num frame#coerce);
diff --git a/ide/coq.ml b/ide/coq.ml
index 6059f065..d318e339 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 9537 2007-01-26 10:05:04Z corbinea $ *)
+(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *)
open Vernac
open Vernacexpr
@@ -152,6 +152,7 @@ let interp verbosely s =
| VernacFixpoint _
| VernacCoFixpoint _
| VernacEndProof _
+ | VernacScheme _
-> Options.make_silent (not verbosely)
| _ -> ()
end;
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fb650cbf..fdc344e8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 9307 2006-10-28 18:48:48Z herbelin $ *)
+(* $Id: coqide.ml 10220 2007-10-12 13:25:54Z notin $ *)
open Preferences
open Vernacexpr
@@ -1719,9 +1719,10 @@ let create_input_tab filename =
let v_box = GPack.hbox ~homogeneous:false () in
let _ = GMisc.image ~packing:v_box#pack () in
let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
+ let appendp x = ignore ((notebook ())#append_page
+ ~tab_label:v_box#coerce x) in
let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
- ~packing:((notebook ())#append_page
- ~tab_label:v_box#coerce) ()
+ ~packing:appendp ()
in
let sw1 = GBin.scrolled_window
~vpolicy:`AUTOMATIC
@@ -2035,8 +2036,8 @@ let main files =
!flash_info "Cannot print: this buffer has no name"
| Some f ->
let cmd =
- "cd " ^ Filename.dirname f ^ "; " ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
+ !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^
" | " ^ !current.cmd_print
in
let s,_ = run_command av#insert_message cmd in
@@ -2063,8 +2064,8 @@ let main files =
| _ -> assert false
in
let cmd =
- "cd " ^ Filename.dirname f ^ "; " ^
- !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+ "cd " ^ (Filename.quote (Filename.dirname f)) ^ "; " ^
+ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
!flash_info (cmd ^
@@ -2411,7 +2412,7 @@ let main files =
| Some f ->
save_f ();
let l,r = !current.cmd_editor in
- let _ = run_command av#insert_message (l ^ f ^ r) in
+ let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in
av#revert)
in
let _ = edit_f#add_separator () in
@@ -2857,7 +2858,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
| Some f ->
let s,res = run_command
av#insert_message
- (!current.cmd_coqc ^ " " ^ f)
+ (!current.cmd_coqc ^ " " ^ (Filename.quote f))
in
if s = Unix.WEXITED 0 then
!flash_info (f ^ " successfully compiled")
@@ -2877,11 +2878,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let make_f () =
let v = get_active_view () in
let av = out_some v.analyzed_view in
+ match av#filename with
+ | None ->
+ !flash_info "Cannot print: this buffer has no name"
+ | Some f ->
+ let cmd =
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
(*
save_f ();
*)
av#insert_message "Command output:\n";
- let s,res = run_command av#insert_message !current.cmd_make in
+ let s,res = run_command av#insert_message cmd in
last_make := res;
last_make_index := 0;
!flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
@@ -2937,9 +2944,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let coq_makefile_f () =
let v = get_active_view () in
let av = out_some v.analyzed_view in
- let s,res = run_command av#insert_message !current.cmd_coqmakefile in
- !flash_info
- (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ match av#filename with
+ | None ->
+ !flash_info "Cannot make makefile: this buffer has no name"
+ | Some f ->
+ let cmd =
+ "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
+ let s,res = run_command av#insert_message cmd in
+ !flash_info
+ (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
in
@@ -3313,7 +3326,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
\nContributors : Jean-Christophe Filliâtre\
\n Pierre Letouzey, Claude Marché\n\
\nFeature wish or bug report: use Web interface\n\
- \n\thttp://coq.inria.fr/bin/coq-bugs\n\
+ \n\thttp://logical.futurs.inria.fr/coq-bugs\n\
\nVersion information\
\n-------------------\n"
in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 349e8629..b9d7694f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: constrextern.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
(*i*)
open Pp
@@ -923,6 +923,8 @@ let rec raw_of_pat env = function
| PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+ | PCase (_,PMeta None,tm,[||]) ->
+ RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
| PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
let brns = Array.to_list cstr_nargs in
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 79a217a1..0c3ffd0c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *)
+(* $Id: coqlib.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
open Util
open Pp
@@ -236,6 +236,7 @@ let coq_I = lazy_init_constant ["Logic"] "I"
(* Connectives *)
let coq_not = lazy_init_constant ["Logic"] "not"
let coq_and = lazy_init_constant ["Logic"] "and"
+let coq_conj = lazy_init_constant ["Logic"] "conj"
let coq_or = lazy_init_constant ["Logic"] "or"
let coq_ex = lazy_init_constant ["Logic"] "ex"
@@ -246,6 +247,7 @@ let build_coq_I () = Lazy.force coq_I
let build_coq_False () = Lazy.force coq_False
let build_coq_not () = Lazy.force coq_not
let build_coq_and () = Lazy.force coq_and
+let build_coq_conj () = Lazy.force coq_conj
let build_coq_or () = Lazy.force coq_or
let build_coq_ex () = Lazy.force coq_ex
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index c81d72de..7254800c 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqlib.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: coqlib.mli 10067 2007-08-09 17:13:16Z msozeau $ i*)
(*i*)
open Names
@@ -129,6 +129,7 @@ val build_coq_not : constr delayed
(* Conjunction *)
val build_coq_and : constr delayed
+val build_coq_conj : constr delayed
(* Disjunction *)
val build_coq_or : constr delayed
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2f17d659..00901686 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 9421 2006-12-08 16:00:53Z barras $ *)
+(* $Id: inductive.ml 10173 2007-10-04 13:02:56Z herbelin $ *)
open Util
open Names
@@ -656,21 +656,32 @@ let check_one_fix renv recpos def =
let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
match kind_of_term f with
| Rel p ->
- List.iter (check_rec_call renv) l;
(* Test if [p] is a fixpoint (recursive call) *)
if renv.rel_min <= p & p < renv.rel_min+nfi then
- (* the position of the invoked fixpoint: *)
- let glob = renv.rel_min+nfi-1-p in
- (* the decreasing arg of the rec call: *)
- let np = recpos.(glob) in
- if List.length l <= np then error_partial_apply renv glob
- else
- (match list_chop np l with
- (la,(z::lrest)) ->
- (* Check the decreasing arg is smaller *)
- if not (check_is_subterm renv z) then
- error_illegal_rec_call renv glob z
- | _ -> assert false)
+ begin
+ List.iter (check_rec_call renv) l;
+ (* the position of the invoked fixpoint: *)
+ let glob = renv.rel_min+nfi-1-p in
+ (* the decreasing arg of the rec call: *)
+ let np = recpos.(glob) in
+ if List.length l <= np then error_partial_apply renv glob
+ else
+ match list_chop np l with
+ (la,(z::lrest)) ->
+ (* Check the decreasing arg is smaller *)
+ if not (check_is_subterm renv z) then
+ error_illegal_rec_call renv glob z
+ | _ -> assert false
+ end
+ else
+ begin
+ match pi2 (lookup_rel p renv.env) with
+ | None ->
+ List.iter (check_rec_call renv) l
+ | Some c ->
+ try List.iter (check_rec_call renv) l
+ with FixGuardError _ -> check_rec_call renv (applist(c,l))
+ end
| Case (ci,p,c_0,lrest) ->
List.iter (check_rec_call renv) (c_0::p::l);
@@ -736,9 +747,19 @@ let check_one_fix renv recpos def =
let renv' = push_fix_renv renv recdef in
Array.iter (check_rec_call renv') bodies
- | (Ind _ | Construct _ | Var _ | Sort _) ->
+ | (Ind _ | Construct _ | Sort _) ->
List.iter (check_rec_call renv) l
+ | Var id ->
+ begin
+ match pi2 (lookup_named id renv.env) with
+ | None ->
+ List.iter (check_rec_call renv) l
+ | Some c ->
+ try List.iter (check_rec_call renv) l
+ with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+ end
+
(* l is not checked because it is considered as the meta's context *)
| (Evar _ | Meta _) -> ()
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 7ea3ff66..372d2be3 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -8,10 +8,24 @@
(* Compatibility file depending on ocaml version *)
-(* IFDEF not available in 3.06; use ifdef instead *)
-
(* type loc is different in 3.08 *)
-ifdef OCAML_308 then
+
+IFDEF OCAML309 THEN DEFINE OCAML308 END
+
+IFDEF CAMLP5 THEN
+module M = struct
+type loc = Stdpp.location
+let dummy_loc = Stdpp.dummy_loc
+let make_loc = Stdpp.make_loc
+let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else Stdpp.encl_loc loc1 loc2
+type token = string*string
+type lexer = token Token.glexer
+let using l x = l.Token.tok_using x
+end
+ELSE IFDEF OCAML308 THEN
module M = struct
type loc = Token.flocation
let dummy_loc = Token.dummy_loc
@@ -24,16 +38,34 @@ let unloc (b,e) =
assert (dummy_loc = (b,e) or make_loc loc = (b,e));
*)
loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
end
-else
+ELSE
module M = struct
type loc = int * int
let dummy_loc = (0,0)
let make_loc x = x
let unloc x = x
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
end
+END
+END
type loc = M.loc
let dummy_loc = M.dummy_loc
let unloc = M.unloc
let make_loc = M.make_loc
+let join_loc = M.join_loc
+type token = M.token
+type lexer = M.lexer
+let using = M.using
diff --git a/lib/options.ml b/lib/options.ml
index c46857e3..53a7e9cf 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: options.ml 9191 2006-09-29 15:45:42Z courtieu $ *)
+(* $Id: options.ml 10105 2007-08-30 16:53:32Z herbelin $ *)
open Util
@@ -121,4 +121,4 @@ let browser_cmd_fmt =
Not_found ->
if Sys.os_type = "Win32"
then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
- else "netscape -remote \"OpenURL(", ")\""
+ else "firefox -remote \"OpenURL(", ")\""
diff --git a/lib/util.ml b/lib/util.ml
index bf70acc7..16d73430 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 9766 2007-04-13 13:26:28Z herbelin $ *)
+(* $Id: util.ml 10185 2007-10-06 18:05:13Z herbelin $ *)
open Pp
@@ -32,9 +32,7 @@ type 'a located = loc * 'a
let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
+let join_loc = Compat.join_loc
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 12c0ea1d..2731fc90 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: argextend.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
open Genarg
open Q_util
open Q_coqast
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let join_loc = Util.join_loc
let loc = Util.dummy_loc
let default_loc = <:expr< Util.dummy_loc >>
@@ -226,7 +226,7 @@ EXTEND
let t, g = interp_entry_name loc e sep in (g, Some (s,t))
| s = STRING ->
if String.length s > 0 && Util.is_letter s.[0] then
- Pcoq.lexer.Token.using ("", s);
+ Compat.using Pcoq.lexer ("", s);
(<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
] ]
;
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 5dda69ba..4216899b 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*)
+(*i $Id: egrammar.mli 10185 2007-10-06 18:05:13Z herbelin $ i*)
(*i*)
open Util
@@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit
type grammar_tactic_production =
| TacTerm of string
| TacNonTerm of
- loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+ loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
val extend_tactic_grammar :
string -> grammar_tactic_production list list -> unit
@@ -61,7 +61,7 @@ val get_extend_vernac_grammars :
(*
val reset_extend_grammars_v8 : unit -> unit
*)
-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
val recover_notation_grammar :
notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6a9388b2..cdd484e7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *)
+(* $Id: g_vernac.ml4 10067 2007-08-09 17:13:16Z msozeau $ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Pp
@@ -143,7 +143,9 @@ GEXTEND Gram
VernacFixpoint (recs,Options.boxed_definitions())
| "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
VernacCoFixpoint (corecs,false)
- | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
+ | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
+ | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
+ l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
;
gallina_ext:
[ [ b = record_token; oc = opt_coercion; name = identref;
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 2f31c0b6..ce284454 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_xml.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: g_xml.ml4 10090 2007-08-24 10:53:53Z herbelin $ *)
open Pp
open Util
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index f7adfdd8..bf3cb084 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.ml4 9333 2006-11-02 13:59:14Z barras $ i*)
+(*i $Id: pcoq.ml4 10185 2007-10-06 18:05:13Z herbelin $ i*)
open Pp
open Util
@@ -29,6 +29,29 @@ open Ppextend
we unfreeze the state of the lexer. This restores the behaviour of the
lexer. B.B. *)
+IFDEF CAMLP5 THEN
+
+let lexer = {
+ Token.tok_func = Lexer.func;
+ Token.tok_using = Lexer.add_token;
+ Token.tok_removing = (fun _ -> ());
+ Token.tok_match = Token.default_match;
+ (* Token.parse = Lexer.tparse; *)
+ Token.tok_comm = None;
+ Token.tok_text = Lexer.token_text }
+
+module L =
+ struct
+ type te = string * string
+ let lexer = lexer
+ end
+
+(* The parser of Coq *)
+
+module G = Grammar.GMake(L)
+
+ELSE
+
let lexer = {
Token.func = Lexer.func;
Token.using = Lexer.add_token;
@@ -45,6 +68,8 @@ module L =
module G = Grammar.Make(L)
+END
+
let grammar_delete e rls =
List.iter
(fun (_,_,lev) ->
@@ -95,7 +120,7 @@ type ext_kind =
| ByGrammar of
grammar_object G.Entry.e * Gramext.position option *
(string option * Gramext.g_assoc option *
- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+ (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
| ByGEXTEND of (unit -> unit) * (unit -> unit)
let camlp4_state = ref []
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1fe8c122..681a6b2c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*)
+(*i $Id: pcoq.mli 10185 2007-10-06 18:05:13Z herbelin $ i*)
open Util
open Names
@@ -20,9 +20,9 @@ open Libnames
(* The lexer and parser of Coq. *)
-val lexer : Token.lexer
+val lexer : Compat.lexer
-module Gram : Grammar.S with type te = Token.t
+module Gram : Grammar.S with type te = Compat.token
(* The superclass of all grammar entries *)
type grammar_object
@@ -42,7 +42,7 @@ val get_constr_entry :
val grammar_extend :
grammar_object Gram.Entry.e -> Gramext.position option ->
(string option * Gramext.g_assoc option *
- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+ (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
-> unit
val remove_grammars : int -> unit
@@ -210,7 +210,7 @@ module Vernac_ :
(* Binding entry names to campl4 entries *)
val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
- bool -> constr_production_entry -> Token.t Gramext.g_symbol
+ bool -> constr_production_entry -> Compat.token Gramext.g_symbol
(* Registering/resetting the level of an entry *)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 275e179e..92c6715e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: ppconstr.ml 10087 2007-08-24 10:39:30Z herbelin $ *)
(*i*)
open Util
@@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
let pr_delimiters key strm =
strm ++ str ("%"^key)
-let pr_located pr ((b,e),x) =
- if Options.do_translate() && (b,e)<>dummy_loc then
- let (b,e) = unloc (b,e) in
+let pr_located pr (loc,x) =
+ if Options.do_translate() && loc<>dummy_loc then
+ let (b,e) = unloc loc in
comment b ++ pr x ++ comment e
else pr x
@@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function
| CHole _ -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
if loc <> dummy_loc then
let (b,_) = unloc loc in
pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f9b8c425..77f0d5cb 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *)
+(* $Id: ppvernac.ml 10087 2007-08-24 10:39:30Z herbelin $ *)
open Pp
open Names
@@ -28,7 +28,7 @@ open Tacinterp
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
if loc <> dummy_loc then
let (b,_) = unloc loc in
pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
@@ -39,7 +39,7 @@ let string_of_fqid fqid =
let pr_fqid fqid = str (string_of_fqid fqid)
-let pr_lfqid (_,_ as loc,fqid) =
+let pr_lfqid (loc,fqid) =
if loc <> dummy_loc then
let (b,_) = unloc loc in
pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
@@ -602,6 +602,11 @@ let rec pr_vernac = function
| VernacScheme l ->
hov 2 (str"Scheme" ++ spc() ++
prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l)
+ | VernacCombinedScheme (id, l) ->
+ hov 2 (str"Combined Scheme" ++ spc() ++
+ pr_lident id ++ spc() ++ str"from" ++ spc() ++
+ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l)
+
(* Gallina extensions *)
| VernacRecord (b,(oc,name),ps,s,c,fs) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 23787f4c..9f828c96 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *)
+(* $Id: q_coqast.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
open Util
open Names
@@ -19,13 +19,18 @@ let purge_str s =
if String.length s == 0 || s.[0] <> '$' then s
else String.sub s 1 (String.length s - 1)
+IFDEF OCAML308 THEN DEFINE NOP END
+IFDEF OCAML309 THEN DEFINE NOP END
+IFDEF CAMLP5 THEN DEFINE NOP END
+
let anti loc x =
let e =
let loc =
- ifdef OCAML_308 then
+ IFDEF NOP THEN
loc
- else
- (1, snd loc - fst loc)
+ ELSE
+ (1, snd loc - fst loc)
+ END
in <:expr< $lid:purge_str x$ >>
in
<:expr< $anti:e$ >>
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 2ef56907..552c144a 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: q_util.ml4 9333 2006-11-02 13:59:14Z barras $ *)
+(* $Id: q_util.ml4 10087 2007-08-24 10:39:30Z herbelin $ *)
(* This file defines standard combinators to build ml expressions *)
@@ -37,18 +37,18 @@ let mlexpr_of_list f l =
List.fold_right
(fun e1 e2 ->
let e1 = f e1 in
- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< [$e1$ :: $e2$] >>)
l (let loc = dummy_loc in <:expr< [] >>)
let mlexpr_of_pair m1 m2 (a1,a2) =
let e1 = m1 a1 and e2 = m2 a2 in
- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
<:expr< ($e1$, $e2$) >>
let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in
+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
<:expr< ($e1$, $e2$, $e3$) >>
(* We don't give location for tactic quotation! *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 73d41465..2dfe489e 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -6,14 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: tacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *)
+open Util
open Genarg
open Q_util
open Q_coqast
open Argextend
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
let loc = Util.dummy_loc
let default_loc = <:expr< Util.dummy_loc >>
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 7cf542fe..4847f385 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -6,14 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *)
+(* $Id: vernacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *)
+open Util
open Genarg
open Q_util
open Q_coqast
open Argextend
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
let loc = Util.dummy_loc
let default_loc = <:expr< Util.dummy_loc >>
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 58dda021..1f7bdad3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
+(* $Id: cases.ml 10071 2007-08-10 15:34:41Z herbelin $ *)
open Util
open Names
@@ -1021,18 +1021,18 @@ let abstract_predicate env sigma indf cur tms = function
(* Depending on whether the predicate is dependent or not, and has real
args or not, we lift it to make room for [sign] *)
(* Even if not intrinsically dep, we move the predicate into a dep one *)
- let sign,k =
+ let sign,q =
if names = [] & n <> 1 then
(* Real args were not considered *)
(if dep<>Anonymous then
- ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
+ (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign)
else
- (sign,n))
+ sign),n
else
(* Real args are OK *)
- (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
- if dep<>Anonymous then 0 else 1) in
- let pred = lift_predicate k pred in
+ (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in
+ let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in
+ let pred = liftn_predicate q k pred in
let pred = extract_predicate [] (pred,tms) in
(true, it_mkLambda_or_LetIn_name env pred sign)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4a2e5ee3..29ec7904 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: detyping.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
open Pp
open Util
@@ -241,7 +241,9 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
| [] -> [[],rhs]
| na::nal ->
match kind_of_term c with
- | Case (ci,_,c,cl) when c = mkRel (list_index na (snd e)) ->
+ | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
+ & (* don't contract if p dependent *)
+ computable p (ci.ci_pp_info.ind_nargs) ->
let clauses = build_tree na isgoal e ci cl in
List.flatten
(List.map (fun (pat,rhs) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 92617820..64e9ebec 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *)
+(* $Id: tacred.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
open Pp
open Util
@@ -358,12 +358,11 @@ let reduce_fix_use_function f whfun fix stack =
Reduced (contract_fix_use_function f fix,stack')
| _ -> NotReducible)
-let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
+let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j = match f j with
| None -> mkCoFix(j,typedbodies)
| Some c -> c in
-(* match List.nth names j with Name id -> f id | _ -> assert false in*)
let subbodies = list_tabulate make_Fi nbodies in
substl (List.rev subbodies) bodies.(bodynum)
@@ -372,19 +371,27 @@ let reduce_mind_case_use_function func env mia =
| Construct(ind_sp,i) ->
let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1), real_cargs)
- | CoFix (_,(names,_,_) as cofix) ->
- let build_fix_name i =
- match names.(i) with
- | Name id ->
- if isConst func then
- let (mp,dp,_) = repr_con (destConst func) in
- let kn = make_con mp dp (label_of_id id) in
- (match constant_opt_value env kn with
- | None -> None
- | Some _ -> Some (mkConst kn))
- else None
- | Anonymous -> None in
- let cofix_def = contract_cofix_use_function build_fix_name cofix in
+ | CoFix (bodynum,(names,_,_) as cofix) ->
+ let build_cofix_name =
+ if isConst func then
+ let (mp,dp,_) = repr_con (destConst func) in
+ fun i ->
+ if i = bodynum then Some func
+ else match names.(i) with
+ | Anonymous -> None
+ | Name id ->
+ (* In case of a call to another component of a block of
+ mutual inductive, try to reuse the global name if
+ the block was indeed initially built as a global
+ definition *)
+ let kn = make_con mp dp (label_of_id id) in
+ try match constant_opt_value env kn with
+ | None -> None
+ | Some _ -> Some (mkConst kn)
+ with Not_found -> None
+ else
+ fun _ -> None in
+ let cofix_def = contract_cofix_use_function build_cofix_name cofix in
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index cb46ab19..3cb3c11b 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqmktop.ml 9496 2007-01-17 15:22:11Z herbelin $ *)
+(* $Id: coqmktop.ml 10192 2007-10-08 00:33:39Z letouzey $ *)
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
The command line contains options specific to coqmktop, options for the
@@ -32,7 +32,10 @@ let ide = split_list Tolink.ide
(* 3. Toplevel objects *)
let camlp4topobjs =
- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+ if Coq_config.camlp4 = "camlp5" then
+ ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+ else
+ ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
let topobjs = camlp4topobjs
let gramobjs = []
@@ -310,7 +313,7 @@ let main () =
(* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
let args = if !top then args @ [ "topstart.cmo" ] else args in
(* Now, with the .cma, we MUST use the -linkall option *)
- let command = String.concat " " (prog::args) in
+ let command = String.concat " " (prog::"-rectypes"::args) in
if !echo then
begin
print_endline command;
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index c14462eb..9c23dda5 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
+(* $Id: setoid_replace.ml 10213 2007-10-10 13:05:59Z letouzey $ *)
open Tacmach
open Proof_type
@@ -819,15 +819,16 @@ let new_morphism m signature id hook =
try find_relation_class output'
with Not_found -> errorlabstrm "Add Morphism"
(str "Not a valid signature: " ++ pr_lconstr output' ++
- str " is neither a registered relation nor the Leibniz " ++
- str " equality.") in
+ str " is neither a registered relation nor the Leibniz " ++
+ str " equality.") in
let rel_a,rel_quantifiers_no =
match rel with
Relation rel -> rel.rel_a, rel.rel_quantifiers_no
| Leibniz (Some t) -> t, 0
- | Leibniz None -> assert false in
+ | Leibniz None -> let _,t = decompose_prod typ in t, 0 in
let rel_a_n =
- clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
+ clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a
+ in
try
let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
let argsrev,_ = decompose_prod output_rel_a_n in
@@ -1890,47 +1891,49 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_
| Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
in
try
- let relation =
- match relation with
- Some rel ->
- (try
- match find_relation_class rel with
- Relation sa -> sa
- | Leibniz _ -> raise Optimize
- with
- Not_found ->
- errorlabstrm "Setoid_rewrite"
- (pr_lconstr rel ++ str " is not a registered relation."))
- | None ->
- match default_relation_for_carrier (pf_type_of gl c1) with
- Relation sa -> sa
- | Leibniz _ -> raise Optimize
- in
- let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
- let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in
- let replace dir eq =
- tclTHENS (assert_tac false Anonymous eq)
- [onLastHyp (fun id ->
- tclTHEN
- (rewrite_tac dir (mkVar id) ~new_goals)
- (clear [id]));
- try_prove_eq_tac]
- in
- tclORELSE
- (replace true eq_left_to_right) (replace false eq_right_to_left) gl
- with
- Optimize -> (* (!replace tac_opt c1 c2) gl *)
- let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in
- tclTHENS (assert_tac false Anonymous eq)
- [onLastHyp (fun id ->
- tclTHEN
- (rewrite_tac false (mkVar id) ~new_goals)
- (clear [id]));
- try_prove_eq_tac] gl
+ let carrier,args = decompose_app (pf_type_of gl c1) in
+ let relation =
+ match relation with
+ Some rel ->
+ (try
+ match find_relation_class rel with
+ Relation sa -> if not (eq_constr carrier sa.rel_a) then
+ errorlabstrm "Setoid_rewrite"
+ (str "the carrier of " ++ pr_lconstr rel ++
+ str " does not match the type of " ++ pr_lconstr c1);
+ sa
+ | Leibniz _ -> raise Optimize
+ with
+ Not_found ->
+ errorlabstrm "Setoid_rewrite"
+ (pr_lconstr rel ++ str " is not a registered relation."))
+ | None ->
+ match default_relation_for_carrier (pf_type_of gl c1) with
+ Relation sa -> sa
+ | Leibniz _ -> raise Optimize
+ in
+ let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in
+ let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in
+ let replace dir eq =
+ tclTHENS (assert_tac false Anonymous eq)
+ [onLastHyp (fun id ->
+ tclTHEN
+ (rewrite_tac dir (mkVar id) ~new_goals)
+ (clear [id]));
+ try_prove_eq_tac]
+ in
+ tclORELSE
+ (replace true eq_left_to_right) (replace false eq_right_to_left) gl
+ with
+ Optimize -> (* (!replace tac_opt c1 c2) gl *)
+ let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in
+ tclTHENS (assert_tac false Anonymous eq)
+ [onLastHyp (fun id ->
+ tclTHEN
+ (rewrite_tac false (mkVar id) ~new_goals)
+ (clear [id]));
+ try_prove_eq_tac] gl
-
-
-
let setoid_replace = general_setoid_replace general_s_rewrite
let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl =
general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl
@@ -1970,11 +1973,22 @@ let setoid_symmetry gl =
Optimize -> symmetry_red true gl
let setoid_symmetry_in id gl =
- let new_hyp =
- let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
- mkApp (he, [| c2 ; c1 |])
- in
- cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
+ let ctype = pf_type_of gl (mkVar id) in
+ let binders,concl = Sign.decompose_prod_assum ctype in
+ let (equiv, args) = decompose_app concl in
+ let rec split_last_two = function
+ | [c1;c2] -> [],(c1, c2)
+ | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
+ | _ -> error "The term provided is not an equivalence"
+ in
+ let others,(c1,c2) = split_last_two args in
+ let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
+ let new_hyp' = mkApp (he, [| c2 ; c1 |]) in
+ let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
+ tclTHENS (cut new_hyp)
+ [ intro_replacing id;
+ tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ]
+ gl
let setoid_transitivity c gl =
try
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac6a396f..37b3cbcb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: tacinterp.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
open Constrintern
open Closure
@@ -436,9 +436,16 @@ let rec intern_intro_pattern lf ist = function
and intern_case_intro_pattern lf ist =
List.map (List.map (intern_intro_pattern lf ist))
-let intern_quantified_hypothesis ist x =
- (* We use identifier both for variables and quantified hyps (no way to
- statically check the existence of a quantified hyp); thus nothing to do *)
+let intern_quantified_hypothesis ist = function
+ | AnonHyp n -> AnonHyp n
+ | NamedHyp id ->
+ (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
+ NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
+
+let intern_binding_name ist x =
+ (* We use identifier both for variables and binding names *)
+ (* Todo: consider the body of the lemma to which the binding refer
+ and if a term w/o ltac vars, check the name is indeed quantified *)
x
let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
@@ -453,7 +460,7 @@ let intern_type = intern_constr_gen true
(* Globalize bindings *)
let intern_binding ist (loc,b,c) =
- (loc,intern_quantified_hypothesis ist b,intern_constr ist c)
+ (loc,intern_binding_name ist b,intern_constr ist c)
let intern_bindings ist = function
| NoBindings -> NoBindings
@@ -1465,8 +1472,17 @@ let interp_quantified_hypothesis ist = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
- with Not_found
- | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*)
+ with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _
+ -> NamedHyp id
+
+let interp_binding_name ist = function
+ | AnonHyp n -> AnonHyp n
+ | NamedHyp id ->
+ (* If a name is bound, it has to be a quantified hypothesis *)
+ (* user has to use other names for variables if these ones clash with *)
+ (* a name intented to be used as a (non-variable) identifier *)
+ try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+ with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _
-> NamedHyp id
(* Quantified named or numbered hypothesis or hypothesis in context *)
@@ -1495,7 +1511,7 @@ let interp_induction_arg ist gl = function
(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
let interp_binding ist gl (loc,b,c) =
- (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c)
+ (loc,interp_binding_name ist b,pf_interp_constr ist gl c)
let interp_bindings ist gl = function
| NoBindings -> NoBindings
@@ -2349,7 +2365,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacMutualCofix (id,l) ->
TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
| TacCut c -> TacCut (subst_rawconstr subst c)
- | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c)
+ | TacAssert (b,na,c) ->
+ TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
| TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
| TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
| TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 42df990f..fecc8977 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -77,3 +77,22 @@ Theorem discr2 : Some true = Some false -> False.
intros.
congruence.
Qed.
+
+Set Implicit Arguments.
+
+Parameter elt: Set.
+Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}.
+Definition t (A: Set) := elt -> A.
+Definition get (A: Set) (x: elt) (m: t A) := m x.
+Definition set (A: Set) (x: elt) (v: A) (m: t A) :=
+ fun (y: elt) => if elt_eq y x then v else m y.
+Lemma gsident:
+ forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+Proof.
+ intros. unfold get, set. case (elt_eq j i); intro.
+ congruence.
+ auto.
+Qed.
+
+
+ \ No newline at end of file
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index cd9d3669..b6af3abc 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_makefile.ml4 8840 2006-05-22 13:51:14Z notin $ *)
+(* $Id: coq_makefile.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -175,8 +175,8 @@ let variables l =
| _ :: r -> var_aux r
in
section "Variables definitions.";
- print "CAMLP4LIB=`camlp4 -where`\n";
-(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
+ print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n";
+ print "CAMLP4=`basename $CAMLP4LIB`\n";
print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-I $(COQTOP)/library -I $(COQTOP)/parsing \\
-I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
@@ -204,8 +204,8 @@ let variables l =
print "CAMLOPTLINK=ocamlopt\n";
print "COQDEP=$(COQBIN)coqdep -c\n";
print "GRAMMARS=grammar.cma\n";
- print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
- print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+ print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+ print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
var_aux l;
print "\n"
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 89f39b22..e787cdb3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 9808 2007-04-29 07:15:18Z herbelin $ *)
+(* $Id: coqdep.ml 10196 2007-10-08 13:50:39Z notin $ *)
open Printf
open Coqdep_lexer
@@ -108,12 +108,12 @@ let absolute_dir dir =
let absolute_file_name basename odir =
let dir = match odir with Some dir -> dir | None -> "." in
- absolute_dir dir / basename
+ absolute_dir dir // basename
let file_name = function
| (s,None) -> file_concat s
| (s,Some ".") -> file_concat s
- | (s,Some d) -> d / file_concat s
+ | (s,Some d) -> d // file_concat s
let traite_fichier_ML md ext =
try
@@ -165,7 +165,7 @@ let cut_prefix p s =
if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
let canonize f =
- let f' = absolute_dir (Filename.dirname f) / Filename.basename f in
+ let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
match List.filter (fun (_,full) -> f' = full) !vAccu with
| (f,_) :: _ -> f
| _ -> f
@@ -411,7 +411,7 @@ let all_subdirs root_dir log_dir =
let f = readdir dirh in
if f <> "." && f <> ".." then
let file = dir@[f] in
- let filename = phys_dir/f in
+ let filename = phys_dir//f in
if (stat filename).st_kind = S_DIR then begin
add (filename,file);
traverse filename file
@@ -429,7 +429,7 @@ let usage () =
exit 1
let add_coqlib_known dir_name f =
- let complete_name = dir_name/f in
+ let complete_name = dir_name//f in
let lib_name = Filename.basename dir_name in
match try (stat complete_name).st_kind with _ -> S_BLK with
| S_REG ->
@@ -458,7 +458,7 @@ let coqdep () =
match (old_dirname,new_dirname) with
| (d, ".") -> d
| (None,d) -> Some d
- | (Some d1,d2) -> Some (d1/d2)
+ | (Some d1,d2) -> Some (d1//d2)
in
let complete_name = file_name ([name],dirname) in
match try (stat complete_name).st_kind with _ -> S_BLK with
@@ -468,7 +468,7 @@ let coqdep () =
let newdirname =
match dirname with
| None -> name
- | Some d -> d/name
+ | Some d -> d//name
in
try
while true do treat (Some newdirname) (readdir dir) done
@@ -490,7 +490,7 @@ let coqdep () =
| _ -> ()
in
let add_known phys_dir log_dir f =
- let complete_name = phys_dir/f in
+ let complete_name = phys_dir//f in
match try (stat complete_name).st_kind with _ -> S_BLK with
| S_REG ->
if Filename.check_suffix f ".ml" then
@@ -505,7 +505,7 @@ let coqdep () =
else if Filename.check_suffix f ".v" then
let basename = Filename.chop_suffix f ".v" in
let name = log_dir@[basename] in
- let file = phys_dir/basename in
+ let file = phys_dir//basename in
let paths = [name;[basename]] in
List.iter
(fun n -> safe_addQueue clash_v vKnown (n,file)) paths
@@ -546,11 +546,11 @@ let coqdep () =
parse (List.tl (Array.to_list Sys.argv));
List.iter
(fun (s,_) -> add_coqlib_directory s)
- (all_subdirs (!coqlib/"theories") "Coq");
+ (all_subdirs (!coqlib//"theories") "Coq");
List.iter
(fun (s,_) -> add_coqlib_directory s)
- (all_subdirs (!coqlib/"contrib") "Coq");
- add_coqlib_directory (!coqlib/"user-contrib");
+ (all_subdirs (!coqlib//"contrib") "Coq");
+ add_coqlib_directory (!coqlib//"user-contrib");
mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
mlKnown := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
warning_mult ".mli" !mliKnown;
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c63a6a9b..2bf615d3 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 10017 2007-07-18 13:23:55Z notin $ i*)
+(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*)
(*s Utility functions for the scanners *)
@@ -367,7 +367,7 @@ rule coq_bol = parse
coq_bol lexbuf }
| space* "(*"
{ let eol = comment lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
+ if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf }
| eof
{ () }
| _
@@ -578,7 +578,7 @@ and body = parse
| '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }
| '.' space+ { char '.'; char ' '; false }
| "(*" { let eol = comment lexbuf in
- if eol then body_bol lexbuf else body lexbuf }
+ if eol then begin line_break(); body_bol lexbuf end else body lexbuf }
| identifier
{ let s = lexeme lexbuf in
ident s (lexeme_start lexbuf);
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a1860329..a8e0133e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: command.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
open Pp
open Util
@@ -657,6 +657,58 @@ let build_scheme lnamedepindsort =
let _ = List.fold_right2 declare listdecl lrecnames [] in
if_verbose ppnl (recursive_message Fixpoint lrecnames)
+let rec get_concl n t =
+ if n = 0 then t
+ else
+ match kind_of_term t with
+ Prod (_,_,t) -> get_concl (pred n) t
+ | _ -> raise (Invalid_argument "get_concl")
+
+let cut_last l =
+ let rec aux acc = function
+ hd :: [] -> List.rev acc, hd
+ | hd :: tl -> aux (hd :: acc) tl
+ | [] -> raise (Invalid_argument "cut_last")
+ in aux [] l
+
+let build_combined_scheme name schemes =
+ let env = Global.env () in
+ let defs =
+ List.map (fun x ->
+ let refe = Ident x in
+ let qualid = qualid_of_reference refe in
+ let cst = Nametab.locate_constant (snd qualid) in
+ qualid, cst, Typeops.type_of_constant env cst)
+ schemes
+ in
+ let (qid, c, t) = List.hd defs in
+ let nargs =
+ let (_, arity, _) = destProd t in
+ nb_prod arity
+ in
+ let prods = nb_prod t - nargs in
+ let defs, (qid, c, t) = cut_last defs in
+ let (args, concl) = decompose_prod_n prods t in
+ let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in
+ let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+ let relargs = rel_vect 0 prods in
+ let concl_typ, concl_bod =
+ List.fold_right
+ (fun (cst, x) (acct, accb) ->
+ mkApp (coqand, [| x; acct |]),
+ mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |]))
+ concls (concl, mkApp (mkConst c, relargs))
+ in
+ let ctx = List.map (fun (x, y) -> x, None, y) args in
+ let typ = it_mkProd_wo_LetIn concl_typ ctx in
+ let body = it_mkLambda_or_LetIn concl_bod ctx in
+ let ce = { const_entry_body = body;
+ const_entry_type = Some typ;
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions() } in
+ let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in
+ if_verbose ppnl (recursive_message Fixpoint [snd name])
+
(* 4| Goal declaration *)
let start_proof id kind c hook =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index e043f354..d15e90cb 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: command.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: command.mli 10067 2007-08-09 17:13:16Z msozeau $ i*)
(*i*)
open Util
@@ -53,6 +53,8 @@ val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
+val build_combined_scheme : identifier located -> identifier located list -> unit
+
val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3dcb1f58..13f1f1da 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *)
+(* $Id: metasyntax.ml 10192 2007-10-08 00:33:39Z letouzey $ *)
open Pp
open Util
@@ -28,7 +28,7 @@ open Notation
(**********************************************************************)
(* Tokens *)
-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+let cache_token (_,s) = Compat.using Pcoq.lexer ("", s)
let (inToken, outToken) =
declare_object {(default_object "TOKEN") with
@@ -739,7 +739,9 @@ let set_entry_type etyps (x,typ) =
let check_rule_productivity l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
- error "A notation must include at least one symbol"
+ error "A notation must include at least one symbol";
+ if (match l with SProdList _ :: _ -> true | _ -> false) then
+ error "A recursive notation must start with at least one symbol"
let is_not_printable = function
| AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4e6058be..2185d2a0 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: mltop.ml4 9397 2006-11-21 21:50:54Z herbelin $ *)
+(* $Id: mltop.ml4 10185 2007-10-06 18:05:13Z herbelin $ *)
open Util
open Pp
@@ -98,7 +98,7 @@ let dir_ml_load s =
str s; str" to Coq code." >])
(* TO DO: .cma loading without toplevel *)
| WithoutTop ->
- ifdef Byte then
+ IFDEF Byte THEN
let _,gname = where_in_path !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
@@ -108,7 +108,7 @@ let dir_ml_load s =
[Filename.dirname gname]
with | Dynlink.Error a ->
errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
- else ()
+ ELSE () END
| Native ->
errorlabstrm "Mltop.no_load_object"
[< str"Loading of ML object file forbidden in a native Coq" >]
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 39106bbf..fdd30711 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 9432 2006-12-12 09:07:36Z courtieu $ *)
+(* $Id: toplevel.ml 10087 2007-08-24 10:39:30Z herbelin $ *)
open Pp
open Util
@@ -139,16 +139,16 @@ let print_highlight_location ib loc =
(* Functions to report located errors in a file. *)
-let print_location_in_file s inlibrary fname (bp,ep) =
+let print_location_in_file s inlibrary fname loc =
let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
- if (bp,ep) = dummy_loc then
+ if loc = dummy_loc then
(errstrm ++ str", unknown location." ++ fnl ())
else
if inlibrary then
(errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
- str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+ str" characters " ++ Cerrors.print_loc loc ++ fnl ())
else
- let (bp,ep) = unloc (bp,ep) in
+ let (bp,ep) = unloc loc in
let ic = open_in fname in
let rec line_of_pos lin bol cnt =
if cnt < bp then
@@ -172,15 +172,16 @@ let print_command_location ib dloc =
str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
| None -> (mt ())
-let valid_loc dloc (b,e) =
- (b,e) <> dummy_loc
+let valid_loc dloc loc =
+ loc <> dummy_loc
& match dloc with
- | Some (bd,ed) -> bd<=b & e<=ed
+ | Some dloc ->
+ let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
| _ -> true
-let valid_buffer_loc ib dloc (b,e) =
- valid_loc dloc (b,e) &
- let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
+let valid_buffer_loc ib dloc loc =
+ valid_loc dloc loc &
+ let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
otherwise. We trap all exceptions to prevent the error message printing
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb719a21..dd6d7e25 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 9874 2007-06-04 13:46:11Z soubiran $ i*)
+(*i $Id: vernacentries.ml 10067 2007-08-09 17:13:16Z msozeau $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -359,6 +359,8 @@ let vernac_cofixpoint = build_corecursive
let vernac_scheme = build_scheme
+let vernac_combined_scheme = build_combined_scheme
+
(**********************)
(* Modules *)
@@ -1137,6 +1139,7 @@ let interp c = match c with
| VernacFixpoint (l,b) -> vernac_fixpoint l b
| VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
| VernacScheme l -> vernac_scheme l
+ | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
(* Modules *)
| VernacDeclareModule (export,(_,id),bl,mtyo) ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 4c671787..9f51841d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacexpr.ml 9481 2007-01-11 19:17:56Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 10067 2007-08-09 17:13:16Z msozeau $ i*)
open Util
open Names
@@ -199,6 +199,7 @@ type vernac_expr =
| VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
| VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
| VernacScheme of (lident * bool * lreference * sort_expr) list
+ | VernacCombinedScheme of lident * lident list
(* Gallina extensions *)
| VernacRecord of bool (* = Record or Structure *)
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 0e17df28..b067ba1f 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: whelp.ml4 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: whelp.ml4 10105 2007-08-30 16:53:32Z herbelin $ *)
open Options
open Pp
@@ -32,8 +32,30 @@ open Tacmach
(* Coq interface to the Whelp query engine developed at
the University of Bologna *)
+let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080"
+let getter_server_name = ref "http://mowgli.cs.unibo.it:58081"
+
+open Goptions
+
+let _ =
+ declare_string_option
+ { optsync = false;
+ optname = "Whelp server";
+ optkey = (SecondaryTable ("Whelp","Server"));
+ optread = (fun () -> !whelp_server_name);
+ optwrite = (fun s -> whelp_server_name := s) }
+
+let _ =
+ declare_string_option
+ { optsync = false;
+ optname = "Whelp getter";
+ optkey = (SecondaryTable ("Whelp","Getter"));
+ optread = (fun () -> !getter_server_name);
+ optwrite = (fun s -> getter_server_name := s) }
+
+
let make_whelp_request req c =
- "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+ !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
let b = Buffer.create 16