summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:16:06 +0200
commit5c6894942e4de978963144606e89db432c306625 (patch)
treea8f1fe2e658c9ba460f1c9af99393d9af21b2dfd
parent745e0fb3b3bc4c435870f1af25c22d495fac9f29 (diff)
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Merge commit 'upstream/8.2.beta4.svn20080907+dfsg'
-rw-r--r--CHANGES10
-rw-r--r--INSTALL39
-rw-r--r--Makefile31
-rw-r--r--Makefile.build79
-rw-r--r--Makefile.common30
-rw-r--r--checker/check.ml8
-rw-r--r--checker/checker.ml10
-rw-r--r--checker/indtypes.ml15
-rw-r--r--checker/mod_checking.ml132
-rw-r--r--checker/reduction.ml14
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--config/Makefile.template7
-rw-r--r--config/coq_config.mli4
-rwxr-xr-xconfigure35
-rw-r--r--contrib/micromega/coq_micromega.ml4
-rw-r--r--contrib/subtac/subtac_coercion.ml30
-rw-r--r--debian/changelog6
-rw-r--r--dev/base_include1
-rw-r--r--dev/db1
-rw-r--r--dev/doc/build-system.txt5
-rw-r--r--kernel/byterun/coq_fix_code.c10
-rw-r--r--kernel/byterun/coq_fix_code.h2
-rw-r--r--kernel/byterun/coq_gc.h4
-rw-r--r--kernel/byterun/coq_interp.c2
-rw-r--r--kernel/byterun/coq_memory.h10
-rw-r--r--kernel/byterun/coq_values.h4
-rw-r--r--lib/util.ml4
-rw-r--r--man/coq-interface.14
-rw-r--r--man/coq-parser.1 (renamed from man/parser.1)6
-rw-r--r--man/coq-tex.122
-rw-r--r--man/coqdep.110
-rw-r--r--man/coqdoc.138
-rw-r--r--man/coqide.1166
-rw-r--r--man/coqmktop.16
-rw-r--r--man/coqwc.12
-rw-r--r--parsing/prettyp.ml4
-rw-r--r--parsing/printmod.ml12
-rw-r--r--pretyping/classops.ml103
-rw-r--r--pretyping/classops.mli25
-rw-r--r--pretyping/coercion.ml33
-rw-r--r--pretyping/reductionops.ml9
-rw-r--r--pretyping/reductionops.mli15
-rw-r--r--scripts/coqmktop.ml5
-rwxr-xr-xtest-suite/check16
-rw-r--r--test-suite/success/coercions.v21
-rw-r--r--theories/FSets/FMapFacts.v4
-rw-r--r--tools/coqdoc/coqdoc.css15
-rw-r--r--toplevel/class.ml11
48 files changed, 707 insertions, 321 deletions
diff --git a/CHANGES b/CHANGES
index 01a81554..a789796c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -423,6 +423,7 @@ Tools
- New stand-alone .vo files verifier "coqchk".
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
+- The binary "parser" has been renamed to "coq-parser".
Miscellaneous
@@ -432,8 +433,13 @@ Miscellaneous
Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
-- An overhauled build system (new Makefiles); see dev/doc/build-system.txt
-- Add -browser option to configure script
+- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
+- Add -browser option to configure script.
+- Build a shared library for the C part of Coq, and use it by default.
+ Bytecode executables are now pure. The behaviour is configurable with
+ the -coqrunbyteflags configure option.
+- Complexity tests can be skipped by setting the environment variable
+ COQTEST_SKIPCOMPLEXITY.
Changes from V8.1gamma to V8.1
==============================
diff --git a/INSTALL b/INSTALL
index 68cd2faf..626417d6 100644
--- a/INSTALL
+++ b/INSTALL
@@ -2,6 +2,7 @@
INSTALLATION PROCEDURES FOR THE COQ V8.2 SYSTEM
-----------------------------------------------
+
WHAT DO YOU NEED ?
==================
@@ -160,6 +161,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
Disable the Objective Caml compiler warnings. This option has no
effect on the result of the compilation.
+-browser <command>
+ Use <command> to open an URL in a browser. %s must appear in <command>,
+ and will be replaced by the URL.
+
5- Still in the root directory, do
make world
@@ -249,6 +254,7 @@ THE AVAILABLE COMMANDS.
There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html
+
COMMON PROBLEMS.
================
@@ -263,6 +269,9 @@ COMMON PROBLEMS.
not be present on certain systems. To fix that, try to replace
mkdirhier with mkdir -p
+ * See also section on dynamically loaded libraries.
+
+
COMPILING FOR DIFFERENT ARCHITECTURES.
======================================
@@ -308,3 +317,33 @@ MOVING BINARIES OR LIBRARY.
the binaries directory) and -libdir (for the standard library directory) :
coqtop -bindir <new directory> -libdir <new directory>
+
+ See also next section.
+
+
+DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
+======================================================
+
+ Some bytecode executables of Coq use the OCaml runtime, which dynamically
+ loads a shared library (.so or .dll). When it is not installed properly, you
+ can get an error message of this kind:
+
+ Fatal error: cannot load shared library dllcoqrun
+ Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+ In this case, you need either:
+ - to set the CAML_LD_LIBRARY_PATH environment variable to point to the
+ directory where dllcoqrun.so is; this is suitable when you want to run
+ the command a limited number of times in a controlled environment (e.g.
+ during compilation of binary packages);
+ - install dllcoqrun.so in a location listed in the file ld.conf that is in
+ the directory of the standard library of OCaml;
+ - recompile your bytecode executables after reconfiguring the location of
+ of the shared library:
+ ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+ where <path> is the directory where the dllcoqrun.so is installed;
+ - (not recommended) compile bytecode executables with a custom OCaml
+ runtime by using:
+ ./configure -coqrunbyteflags -custom ...
+ be aware that stripping executables generated this way, or performing
+ other executable-specific operations, will make them useless.
diff --git a/Makefile b/Makefile
index 1f770724..1eb7dc85 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 11309 2008-08-06 10:30:35Z herbelin $
+# $Id: Makefile 11387 2008-09-07 21:59:11Z glondu $
# Makefile for Coq
@@ -24,7 +24,14 @@
# by Emacs' next-error.
###########################################################################
-FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or
+export FIND_VCS_CLAUSE:='(' \
+ -name '{arch}' -or \
+ -name '.svn' -or \
+ -name '_darcs' -or \
+ -name '.git' -or \
+ -name 'debian' -or \
+ -name "$${GIT_DIR}" \
+')' -prune -type f -or
FIND_PRINTF_P:=-print | sed 's|^\./||'
export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P))
@@ -43,7 +50,7 @@ export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIN
export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
#export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \
# $(GENVFILES)
-export CFILES := $(shell find kernel/byterun -name '*.c')
+export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) -name '*.c')
export ML4FILESML:= $(ML4FILES:.ml4=.ml)
@@ -148,12 +155,14 @@ cruftclean: ml4clean
indepclean:
rm -f $(GENFILES)
- rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/parser$(EXE)
+ rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
+ rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
- find contrib -name '*.vo' -or -name '*.glob' | xargs rm -f
+ find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
rm -f */*.pp[iox] contrib/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
+ rm -f test-suite/check.log
rm -f glob.dump
rm -f revision
@@ -175,11 +184,11 @@ docclean:
rm -f doc/coq.tex
archclean: clean-ide cleantheories
- rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP)
- rm -f $(COQTOP) $(COQCOPT) $(COQMKTOPOPT)
- rm -f bin/parser.opt$(EXE) bin/coq-interface.opt$(EXE)
- find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f
- rm -f $(TOOLS)
+ rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN)
+ rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
+ rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
+ find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
+ rm -f $(TOOLS) $(CSDPCERT)
clean-ide:
rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
@@ -194,7 +203,7 @@ ml4depclean:
find . -name '*.ml4.d' | xargs rm -f
depclean:
- find . -name '*.d' | xargs rm -f
+ find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f
cleanconfig:
rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
diff --git a/Makefile.build b/Makefile.build
index a5bae4ea..b8d27b22 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile.build 11309 2008-08-06 10:30:35Z herbelin $
+# $Id: Makefile.build 11383 2008-09-07 16:35:13Z glondu $
# Makefile for Coq
@@ -137,10 +137,11 @@ endif
CINCLUDES= -I $(CAMLHLIB)
-# libcoqrun.a
+# libcoqrun.a, dllcoqrun.so
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
- $(AR) rc $(LIBCOQRUN) $(BYTERUN)
+ cd $(dir $(LIBCOQRUN)) && \
+ $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
$(RANLIB) $(LIBCOQRUN)
#coq_jumptbl.h is required only if you have GCC 2.0 or later
@@ -180,7 +181,7 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
-$(COQTOP): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
+$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
LOCALCHKLIBS:=-I checker -I lib -I config -I kernel
@@ -195,7 +196,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
$(CHICKENBYTE): checker/check.cma checker/main.ml
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -custom -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+ $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -204,13 +205,14 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
$(COQMKTOPBYTE): $(COQMKTOPCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma \
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \
$(COQMKTOPCMO) $(OSDEPLIBS)
$(COQMKTOPOPT): $(COQMKTOPCMX)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \
$(COQMKTOPCMX) $(OSDEPLIBS)
+ $(STRIP) $@
$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
@@ -226,11 +228,12 @@ scripts/tolink.ml: Makefile.build Makefile.common
$(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
$(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS)
+ $(STRIP) $@
$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)
@@ -361,13 +364,14 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx)
###########################################################################
ifeq ($(BEST),opt)
-bin/csdpcert$(EXE): $(CSDPCERTCMX)
+contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX)
+ $(STRIP) $@
else
-bin/csdpcert$(EXE): $(CSDPCERTCMO)
+contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
endif
###########################################################################
@@ -448,7 +452,7 @@ install-ide-info:
$(INSTALLLIB) ide/FAQ $(FULLIDELIB)
###########################################################################
-# Pcoq: special binaries for debugging (coq-interface, parser)
+# Pcoq: special binaries for debugging (coq-interface, coq-parser)
###########################################################################
# target to build Pcoq
@@ -464,12 +468,12 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
-bin/parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
+bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \
+ $(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
-bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
+bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
$(SHOW)'OCAMLOPT -o $@'
$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
$(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX)
@@ -496,6 +500,10 @@ install-pcoq-manpages:
# tests
###########################################################################
+validate:: $(BESTCHICKEN) $(ALLVO)
+ $(SHOW)'COQCHK <theories & contrib>'
+ $(BESTCHICKEN) -boot -o -m $(ALLMODS)
+
check:: world
cd test-suite; \
env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
@@ -583,27 +591,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
$(COQDEP): $(COQDEPCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
$(GALLINA): $(GALLINACMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
$(COQTEX): tools/coq-tex.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
$(COQWC): tools/coqwc.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
$(COQDOC): $(COQDOCCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
###########################################################################
# Installation
@@ -617,7 +625,7 @@ $(COQDOC): $(COQDOCCMO)
# You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLCOQLIB=$(COQLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
@@ -630,12 +638,12 @@ install-binaries:: install-$(BEST) install-tools
install-byte::
$(MKDIR) $(FULLBINDIR)
- $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR)
+ $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
install-opt::
$(MKDIR) $(FULLBINDIR)
- $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR)
+ $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
install-tools::
@@ -655,8 +663,16 @@ install-library:
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
- $(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
- find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+ $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
+ifeq ($(BEST),opt)
+ $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
+endif
+ find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+# csdpcert is not meant to be directly called by the user; we install
+# it with libraries
+ -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
+ $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
+ $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
install-library-light:
$(MKDIR) $(FULLCOQLIB)
@@ -699,7 +715,8 @@ install-latex:
source-doc:
if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
- $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) `find . -name "*.ml"`
+ $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \
+ `find . $(FIND_VCS_CLAUSE) -name "*.ml"`
###########################################################################
@@ -716,7 +733,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)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
@rm -f test-grammar test.*
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
@@ -823,8 +840,8 @@ checker/%.cmi: checker/%.mli | checker/%.mli.d
$(HIDE)$(OCAMLC) -c $(CHKBYTEFLAGS) $<
%.o: %.c
- $(SHOW)'CC $<'
- $(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES) -c $<
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
ifdef KEEP_ML4_PREPROCESSED
.PRECIOUS: %.ml4-preprocessed
@@ -875,8 +892,8 @@ endif
$(HIDE)rm -f $*.glob
$(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
ifdef VALIDATE
- $(SHOW)'COQCHK $(shell basename $*)'
- $(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \
+ $(SHOW)'COQCHK $(call vo_to_mod,$@)'
+ $(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
|| ( RV=$$?; rm -f "$@"; exit $${RV} )
endif
diff --git a/Makefile.common b/Makefile.common
index 0a5d4260..a752892d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -23,7 +23,7 @@ COQC:=bin/coqc$(EXE)
COQTOPBYTE:=bin/coqtop.byte$(EXE)
COQTOPOPT:=bin/coqtop.opt$(EXE)
BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
-COQTOP:=bin/coqtop$(EXE)
+COQTOPEXE:=bin/coqtop$(EXE)
CHICKENBYTE:=bin/coqchk.byte$(EXE)
CHICKENOPT:=bin/coqchk.opt$(EXE)
BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
@@ -39,14 +39,14 @@ COQIDE:=bin/coqide$(EXE)
ifeq ($(BEST),opt)
COQBINARIES:= $(COQMKTOP) $(COQC) \
- $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
+ $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
else
COQBINARIES:= $(COQMKTOP) $(COQC) \
- $(COQTOPBYTE) $(COQTOP) $(CHICKENBYTE) $(CHICKEN)
+ $(COQTOPBYTE) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKEN)
endif
OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
-CSDPCERT:=bin/csdpcert$(EXE)
+CSDPCERT:=contrib/micromega/csdpcert$(EXE)
###########################################################################
# tools
@@ -74,7 +74,7 @@ HEVEA:=hevea
HEVEAOPTS:=-fix -exec xxdate.exe
HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
-COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small
+COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOPEXE) -v -sl -small
DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
@@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
# Object and Source files
###########################################################################
-LIBCOQRUN:=kernel/byterun/libcoqrun.a
+COQRUN := coqrun
+LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
+DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so
CLIBS:=unix.cma
@@ -377,9 +379,9 @@ PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
PARSERREQUIRESCMX:=$(LINKCMX)
ifeq ($(BEST),opt)
- COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE)
+ COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE)
else
- COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE)
+ COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
endif
PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
@@ -811,6 +813,12 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
VFILES:= $(ALLVO:.vo=.v)
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
LIBFILESLIGHT:=$(THEORIESLIGHTVO)
@@ -821,10 +829,10 @@ INTERFACEVO:=
MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
- man/coqwc.1 man/coqdoc.1 \
+ man/coqwc.1 man/coqdoc.1 man/coqide.1 \
man/coq_makefile.1 man/coqmktop.1
-PCOQMANPAGES:=man/coq-interface.1 man/parser.1
+PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
parsing/pptactic.ml
@@ -872,7 +880,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
coqlight states pcoq-files check init theories theories-light contrib \
- $(DOC_TARGETS) $(VO_TARGETS)
+ $(DOC_TARGETS) $(VO_TARGETS) validate
# For emacs:
diff --git a/checker/check.ml b/checker/check.ml
index e91516c7..40ac604e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -23,8 +23,7 @@ type section_path = {
dirpath : string list ;
basename : string }
let dir_of_path p =
- make_dirpath
- (id_of_string p.basename :: List.map id_of_string p.dirpath)
+ make_dirpath (List.map id_of_string p.dirpath)
let path_of_dirpath dir =
match repr_dirpath dir with
[] -> failwith "path_of_dirpath"
@@ -166,6 +165,9 @@ let remove_load_path dir =
load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
let add_load_path (phys_path,coq_path) =
+ if !Flags.debug then
+ msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+ str phys_path);
let phys_path = canonical_path_name phys_path in
match list_filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
@@ -224,7 +226,7 @@ let locate_qualified_library qid =
(* Search library in loadpath *)
if qid.dirpath=[] then get_load_paths ()
else
- (* we assume dir is an absolute dirpath *)
+ (* we assume qid is an absolute dirpath *)
load_paths_of_dir_path (dir_of_path qid)
in
if loadpath = [] then raise LibUnmappedDir;
diff --git a/checker/checker.ml b/checker/checker.ml
index 7de25835..1ed094cf 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -191,6 +191,11 @@ let print_usage_channel co command =
-where print Coq's standard library location and exit
-v print Coq version and exit
+ -boot boot mode
+ -o print the list of assumptions
+ -m print the maximum heap size
+
+ -impredicative-set set sort Set impredicative
-h, --help print this list of options
"
@@ -323,10 +328,9 @@ let parse_args() =
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
-
+ | "-boot" :: rem -> boot := true; parse rem
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
-
- | ("-o" | "-output-context") :: rem ->
+ | ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
| "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8c84fb0f..4c9b3d61 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -19,6 +19,21 @@ open Pp
open Declarations
open Environ
+let rec debug_string_of_mp = function
+ | MPfile sl -> string_of_dirpath sl
+ | MPbound uid -> "bound("^string_of_mbid uid^")"
+ | MPself uid -> "self("^string_of_msid uid^")"
+ | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let rec string_of_mp = function
+ | MPfile sl -> string_of_dirpath sl
+ | MPbound uid -> string_of_mbid uid
+ | MPself uid -> string_of_msid uid
+ | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let string_of_mp mp =
+ if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
+
let prkn kn =
let (mp,_,l) = repr_kn kn in
str(string_of_mp mp ^ "." ^ string_of_label l)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ecf8d633..379273af 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
let check_constant_declaration env kn cb =
Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn);
- let env = add_constraints cb.const_constraints env in
+(* let env = add_constraints cb.const_constraints env in*)
let env' = check_named_ctxt env cb.const_hyps in
(match cb.const_type with
NonPolymorphicType ty ->
@@ -47,58 +47,6 @@ let check_constant_declaration env kn cb =
(* Checking modules *)
-let rec add_struct_expr_constraints env = function
- | SEBident _ -> env
-
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
- (add_modtype_constraints env mtb) meb
-
- | SEBstruct (_,structure_body) ->
- List.fold_left
- (fun env (l,item) -> add_struct_elem_constraints env item)
- env
- structure_body
-
- | SEBapply (meb1,meb2,cst) ->
-(* let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
- Univ.pr_universes g++str"============="++fnl());
-*)
- Environ.add_constraints cst
- (add_struct_expr_constraints
- (add_struct_expr_constraints env meb1)
- meb2)
- | SEBwith(meb,With_definition_body(_,cb))->
- Environ.add_constraints cb.const_constraints
- (add_struct_expr_constraints env meb)
- | SEBwith(meb,With_module_body(_,_,cst))->
- Environ.add_constraints cst
- (add_struct_expr_constraints env meb)
-
-and add_struct_elem_constraints env = function
- | SFBconst cb -> Environ.add_constraints cb.const_constraints env
- | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
- | SFBmodule mb -> add_module_constraints env mb
- | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
- | SFBalias (mp,None) -> env
- | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb =
- let env = match mb.mod_expr with
- | None -> env
- | Some meb -> add_struct_expr_constraints env meb
- in
- let env = match mb.mod_type with
- | None -> env
- | Some mtb ->
- add_struct_expr_constraints env mtb
- in
- Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb =
- add_struct_expr_constraints env mtb.typ_expr
-
exception Not_path
let path_of_mexpr = function
@@ -307,19 +255,18 @@ and check_module_type env mty =
check_alias mty.typ_alias sub
and check_module env mb =
- let env' = add_module_constraints env mb in
let sub =
match mb.mod_expr, mb.mod_type with
| None, None ->
anomaly "Mod_typing.translate_module: empty type and expr in module entry"
- | None, Some mtb -> check_modexpr env' mtb
+ | None, Some mtb -> check_modexpr env mtb
| Some mexpr, _ ->
- let sub1 = check_modexpr env' mexpr in
+ let sub1 = check_modexpr env mexpr in
(match mb.mod_type with
| None -> sub1
| Some mte ->
- let sub2 = check_modexpr env' mte in
+ let sub2 = check_modexpr env mte in
check_subtypes env
{typ_expr = mexpr;
typ_strength = None;
@@ -342,21 +289,22 @@ and check_structure_field (s,env) mp lab = function
let mp1 = MPdot(mp,lab) in
let is_fun, sub = Modops.update_subst env msb mp1 in
((if is_fun then s else join s sub),
- Modops.add_module (MPdot(mp,lab)) msb
- (add_module_constraints env msb))
+ Modops.add_module (MPdot(mp,lab)) msb env)
| SFBalias(mp2,cst) ->
+ (* cf Safe_typing.add_alias *)
(try
+ let mp' = MPdot(mp,lab) in
let mp2' = scrape_alias mp2 env in
- let msb = lookup_module mp2' env in
- (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias),
- Option.fold_right add_constraints cst
- (register_alias (MPdot(mp,lab)) mp2 env))
+ let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
+ let sub = update_subst sub (map_mp mp' mp2') in
+ let sub = join_alias sub (map_mp mp' mp2') in
+ let sub = add_mp mp' mp2' sub in
+ (join s sub, register_alias mp' mp2 env)
with Not_found -> failwith "unkown aliased module")
| SFBmodtype mty ->
let kn = MPdot(mp, lab) in
check_module_type env mty;
- (join s mty.typ_alias,
- add_modtype kn mty (add_modtype_constraints env mty))
+ (join s mty.typ_alias, add_modtype kn mty env)
and check_modexpr env mse = match mse with
| SEBident mp ->
@@ -396,3 +344,57 @@ and check_modexpr env mse = match mse with
List.fold_left (fun env (lab,mb) ->
check_structure_field env mp lab mb) (empty_subst,env) msb in
sub
+
+(*
+let rec add_struct_expr_constraints env = function
+ | SEBident _ -> env
+
+ | SEBfunctor (_,mtb,meb) ->
+ add_struct_expr_constraints
+ (add_modtype_constraints env mtb) meb
+
+ | SEBstruct (_,structure_body) ->
+ List.fold_left
+ (fun env (l,item) -> add_struct_elem_constraints env item)
+ env
+ structure_body
+
+ | SEBapply (meb1,meb2,cst) ->
+(* let g = Univ.merge_constraints cst Univ.initial_universes in
+msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
+ Univ.pr_universes g++str"============="++fnl());
+*)
+ Environ.add_constraints cst
+ (add_struct_expr_constraints
+ (add_struct_expr_constraints env meb1)
+ meb2)
+ | SEBwith(meb,With_definition_body(_,cb))->
+ Environ.add_constraints cb.const_constraints
+ (add_struct_expr_constraints env meb)
+ | SEBwith(meb,With_module_body(_,_,cst))->
+ Environ.add_constraints cst
+ (add_struct_expr_constraints env meb)
+
+and add_struct_elem_constraints env = function
+ | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+ | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
+ | SFBmodule mb -> add_module_constraints env mb
+ | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
+ | SFBalias (mp,None) -> env
+ | SFBmodtype mtb -> add_modtype_constraints env mtb
+
+and add_module_constraints env mb =
+ let env = match mb.mod_expr with
+ | None -> env
+ | Some meb -> add_struct_expr_constraints env meb
+ in
+ let env = match mb.mod_type with
+ | None -> env
+ | Some mtb ->
+ add_struct_expr_constraints env mtb
+ in
+ Environ.add_constraints mb.mod_constraints env
+
+and add_modtype_constraints env mtb =
+ add_struct_expr_constraints env mtb.typ_expr
+*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 49f05daf..c398f0a4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -195,6 +195,12 @@ let in_whnf (t,stk) =
| (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true
| FLOCKED -> assert false
+let oracle_order fl1 fl2 =
+ match fl1,fl2 with
+ ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
+ | _, ConstKey _ -> true
+ | _ -> false
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
+ if oracle_order fl1 fl2 then
+ match unfold_reference infos fl1 with
+ | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+ | None ->
+ (match unfold_reference infos fl2 with
+ | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+ | None -> raise NotConvertible)
+ else
match unfold_reference infos fl2 with
| Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
| None ->
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4b156e7e..d5779923 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -31,7 +31,7 @@ let set_engagement c =
let full_add_module dp mb digest =
let env = !genv in
let mp = MPfile dp in
- let env = add_module_constraints env mb in
+ let env = add_constraints mb.mod_constraints env in
let env = Modops.add_module mp mb env in
genv := add_digest env dp digest
@@ -121,7 +121,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
let env = !genv in
check_imports msg_warning dp env depends;
check_engagement env engmt;
- check_module env mb;
+ check_module (add_constraints mb.mod_constraints env) mb;
stamp_library file digest;
(* We drop proofs once checked *)
(* let mb = lighten_module mb in*)
diff --git a/config/Makefile.template b/config/Makefile.template
index fc8af173..e0e7bf0b 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -21,6 +21,10 @@ COQ_CONFIGURED=yes
# Local use (no installation)
LOCAL=LOCALINSTALLATION
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+BUILDLDPATH=
+
# Paths for true installation
# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
# do_Makefile will reside
@@ -28,7 +32,7 @@ LOCAL=LOCALINSTALLATION
# MANDIR=path where to install manual pages
# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
BINDIR="BINDIRDIRECTORY"
-COQLIB="COQLIBDIRECTORY"
+COQLIBINSTALL="COQLIBDIRECTORY"
MANDIR="MANDIRDIRECTORY"
DOCDIR="DOCDIRDIRECTORY"
EMACSLIB="EMACSLIBDIRECTORY"
@@ -58,6 +62,7 @@ COQIDEINCLUDES=LABLGTKINCLUDES
# Objective-Caml compile command
OCAML="OCAMLEXEC"
OCAMLC="BYTECAMLC"
+OCAMLMKLIB="OCAMLMKLIBEXEC"
OCAMLOPT="NATIVECAMLC"
OCAMLDEP="OCAMLDEPEXEC"
OCAMLDOC="OCAMLDOCEXEC"
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 3898a0f3..af943509 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 11313 2008-08-07 11:15:03Z barras $ i*)
+(*i $Id: coq_config.mli 11380 2008-09-07 12:27:27Z glondu $ i*)
val local : bool (* local use (no installation) *)
@@ -24,6 +24,8 @@ val camlp4lib : string (* where is the library of Camlp4 *)
val best : string (* byte/opt *)
val arch : string (* architecture *)
val osdeplibs : string (* OS dependant link options for ocamlc *)
+val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
+
(* val defined : string list (* options for lib/ocamlpp *) *)
diff --git a/configure b/configure
index 2747ee2f..79a772ed 100755
--- a/configure
+++ b/configure
@@ -6,10 +6,13 @@
#
##################################
-VERSION=8.2beta4
+VERSION=8.2
VOMAGIC=08193
STATEMAGIC=19764
-DATE="Aug. 2008"
+DATE="Jun. 2008"
+
+# Create the bin/ directory if non-existent
+test -d bin || mkdir bin
# a local which command for sh
which () {
@@ -32,6 +35,8 @@ usage () {
printf "\tSet installation directory to <dir>\n"
echo "-local"
printf "\tSet installation directory to the current source tree\n"
+ echo "-coqrunbyteflags"
+ printf "\tSet link flags for VM-dependent bytecode\n"
echo "-src"
printf "\tSpecifies the source directory\n"
echo "-bindir"
@@ -83,6 +88,7 @@ usage () {
# Default OCaml binaries
bytecamlc=ocamlc
nativecamlc=ocamlopt
+ocamlmklib=ocamlmklib
ocamlexec=ocaml
ocamldepexec=ocamldep
ocamldocexec=ocamldoc
@@ -104,6 +110,7 @@ ar_exec=ar
ranlib_exec=ranlib
local=false
+coqrunbyteflags_spec=no
src_spec=no
prefix_spec=no
bindir_spec=no
@@ -137,6 +144,9 @@ while : ; do
prefix="$2"
shift;;
-local|--local) local=true;;
+ -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
+ coqrunbyteflags="$2"
+ shift;;
-src|--src) src_spec=yes
COQSRC="$2"
shift;;
@@ -754,6 +764,14 @@ case $coqdocdir_spec/$prefix_spec/$local in
esac;;
esac
+BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
+case $coqrunbyteflags_spec/$local in
+ yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
+ */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
+ *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
+ BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
+esac
+
# case $emacs_spec in
# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
# read EMACS
@@ -774,6 +792,7 @@ echo " Architecture : $ARCH"
if test ! -z "$OS" ; then
echo " Operating system : $OS"
fi
+echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS"
echo " OS dependent libraries : $OSDEPLIBS"
echo " Objective-Caml/Camlp4 version : $CAMLVERSION"
echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN"
@@ -862,9 +881,10 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
let local = $local
-let bindir = "$ESCBINDIR"
-let coqlib = "$ESCLIBDIR"
-let coqtop = "$ESCCOQTOP"
+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
+let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR"
+let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR"
+let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP"
let camldir = "$ESCCAMLDIR"
let camllib = "$ESCCAMLLIB"
let camlp4 = "$CAMLP4"
@@ -909,10 +929,12 @@ chmod a-w "$mlconfig_file"
rm -f "$COQSRC/config/Makefile"
sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
-e "s|COQSRCDIRECTORY|$COQSRC|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
+ -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
-e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
-e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
-e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
@@ -937,6 +959,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|BESTCOMPILER|$best_compiler|" \
-e "s|EXECUTEEXTENSION|$EXE|" \
-e "s|BYTECAMLC|$bytecamlc|" \
+ -e "s|OCAMLMKLIBEXEC|$ocamlmklib|" \
-e "s|NATIVECAMLC|$nativecamlc|" \
-e "s|OCAMLEXEC|$ocamlexec|" \
-e "s|OCAMLDEPEXEC|$ocamldepexec|" \
@@ -994,4 +1017,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 11320 2008-08-07 19:40:59Z notin $
+# $Id: configure 11380 2008-09-07 12:27:27Z glondu $
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 02ff61a1..5ae12394 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -1193,8 +1193,8 @@ let call_csdpcert provername poly =
output_value ch_to (provername,poly : provername * micromega_polys);
close_out ch_to;
let cmdname =
- Filename.concat Coq_config.bindir
- ("csdpcert" ^ Coq_config.exec_extension) in
+ List.fold_left Filename.concat Coq_config.coqlib
+ ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
(try Sys.remove tmp_to with _ -> ());
if c <> 0 then Util.error ("Failed to call csdp certificate generator");
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b046f0b3..4d8f868f 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Util
open Names
@@ -310,8 +310,6 @@ module Coercion = struct
(* Typing operations dealing with coercions *)
- let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
-
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env argl funj =
let rec apply_rec acc typ = function
@@ -339,19 +337,17 @@ module Coercion = struct
(* raise Not_found if no coercion found *)
let inh_pattern_coerce_to loc pat ind1 ind2 =
- let i1 = inductive_class_of ind1 in
- let i2 = inductive_class_of ind2 in
- let p = lookup_pattern_path_between (i1,i2) in
+ let p = lookup_pattern_path_between (ind1,ind2) in
apply_pattern_coercion loc pat p
(* appliquer le chemin de coercions p à hj *)
- let apply_coercion env p hj typ_cl =
+ let apply_coercion env sigma p hj typ_cl =
try
fst (List.fold_left
(fun (ja,typ_cl) i ->
let fv,isid = coercion_value i in
- let argl = (class_args_of typ_cl)@[ja.uj_val] in
+ let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
let jres = apply_coercion_args env argl fv in
(if isid then
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -370,9 +366,9 @@ module Coercion = struct
(isevars',{ uj_val = j.uj_val; uj_type = t })
| _ ->
(try
- let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
- let p = lookup_path_to_fun_from i1 in
- (isevars,apply_coercion env p j t)
+ let t,p =
+ lookup_path_to_fun_from env (evars_of isevars) j.uj_type in
+ (isevars,apply_coercion env (evars_of isevars) p j t)
with Not_found ->
try
let coercef, t = mu env isevars t in
@@ -382,9 +378,8 @@ module Coercion = struct
let inh_tosort_force loc env isevars j =
try
- let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
- let p = lookup_path_to_sort_from i1 in
- let j1 = apply_coercion env p j t in
+ let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in
+ let j1 = apply_coercion env (evars_of isevars) p j t in
(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
with Not_found ->
error_not_a_type_loc loc env (evars_of isevars) j
@@ -417,12 +412,11 @@ module Coercion = struct
else
let v', t' =
try
- let t1,i1 = class_of1 env (evars_of evd) c1 in
- let t2,i2 = class_of1 env (evars_of evd) t in
- let p = lookup_path_between (i2,i1) in
+ let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
match v with
Some v ->
- let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+ let j = apply_coercion env (evars_of evd) p
+ {uj_val = v; uj_type = t} t2 in
Some j.uj_val, j.uj_type
| None -> None, t
with Not_found -> raise NoCoercion
diff --git a/debian/changelog b/debian/changelog
index 47eeeab1..fdef3f28 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+coq (8.2~beta4.svn20080907+dfsg-1) UNRELEASED; urgency=low
+
+ * [113b703] New upstream SVN snapshot
+
+ -- Stephane Glondu <steph@glondu.net> Mon, 08 Sep 2008 00:15:39 +0200
+
coq (8.2~beta4+dfsg-2) experimental; urgency=low
* [45cca7f] Add non-native-archs.dpatch; fixes FTBFS on non-native
diff --git a/dev/base_include b/dev/base_include
index 398f60d2..0b7a0b67 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,6 +29,7 @@
#install_printer (* qualid *) ppqualid;;
#install_printer (* kernel_name *) ppkn;;
#install_printer (* constant *) ppcon;;
+#install_printer (* cl_index *) ppclindex;;
#install_printer (* constr *) print_pure_constr;;
#install_printer (* patch *) ppripos;;
#install_printer (* values *) ppvalues;;
diff --git a/dev/db b/dev/db
index 6221462a..81878570 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppkn
install_printer Top_printers.ppcon
install_printer Top_printers.ppsp
install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
install_printer Top_printers.ppbigint
install_printer Top_printers.pppattern
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index c9571f7c..9362aeeb 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -253,9 +253,8 @@ config/Makefile looks like it contains a lot of unused variables,
clean that up (are any maybe used by nightly scripts on
pauillac?). Also, the COQTOP variable from config/Makefile (and used
in contribs) has a very poorly chosen name, because "coqtop" is the
-name of a Coq executable! For example, in the Coq makefile it is
-immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or
-COQTREE or COQDIR or ...
+name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
+to refer to that executable.
Promote the granular .glob handling to official way of doing things
for Coq developments, that is implement it in coq_makefile and the
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 55b907ad..5d302660 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -13,11 +13,11 @@
#include <stdio.h>
#include <stdlib.h>
-#include <config.h>
-#include <misc.h>
-#include <mlvalues.h>
-#include <fail.h>
-#include <memory.h>
+#include <caml/config.h>
+#include <caml/misc.h>
+#include <caml/mlvalues.h>
+#include <caml/fail.h>
+#include <caml/memory.h>
#include "coq_instruct.h"
#include "coq_fix_code.h"
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 00345318..c1a4e0ae 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -12,7 +12,7 @@
#ifndef _COQ_FIX_CODE_
#define _COQ_FIX_CODE_
-#include <mlvalues.h>
+#include <caml/mlvalues.h>
void * coq_stat_alloc (asize_t sz);
#ifdef THREADED_CODE
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index ccccbe78..c7b18b90 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -10,8 +10,8 @@
#ifndef _COQ_CAML_GC_
#define _COQ_CAML_GC_
-#include <mlvalues.h>
-#include <alloc.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
typedef void (*scanning_action) (value, value *);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 880e978a..98ef2791 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -21,7 +21,7 @@
#include "coq_values.h"
/*spiwack : imports support functions for 64-bit integers */
-#include "config.h"
+#include <caml/config.h>
#ifdef ARCH_INT64_TYPE
#include "int64_native.h"
#else
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index edd05948..c0093a49 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -11,11 +11,11 @@
#ifndef _COQ_MEMORY_
#define _COQ_MEMORY_
-#include <config.h>
-#include <fail.h>
-#include <misc.h>
-#include <memory.h>
-#include <mlvalues.h>
+#include <caml/config.h>
+#include <caml/fail.h>
+#include <caml/misc.h>
+#include <caml/memory.h>
+#include <caml/mlvalues.h>
#define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 4c631fce..1bf493e2 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -11,8 +11,8 @@
#ifndef _COQ_VALUES_
#define _COQ_VALUES_
-#include <alloc.h>
-#include <mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/mlvalues.h>
#define Default_tag 0
#define Accu_tag 0
diff --git a/lib/util.ml b/lib/util.ml
index 75ee4246..a19cc65b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: util.ml 11350 2008-09-02 15:37:49Z barras $ *)
open Pp
@@ -1361,7 +1361,7 @@ let heap_size () =
let stat = Gc.stat ()
and control = Gc.get () in
let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
- (max_words_total * Sys.word_size / 8)
+ (max_words_total * (Sys.word_size / 8))
let heap_size_kb () = (heap_size () + 1023) / 1024
diff --git a/man/coq-interface.1 b/man/coq-interface.1
index 2ab2bf95..ee013d95 100644
--- a/man/coq-interface.1
+++ b/man/coq-interface.1
@@ -1,7 +1,7 @@
.TH COQ 1 "April 25, 2001"
.SH NAME
-coq-interface \-
+coq\-interface \- Customized Coq toplevel to make user interfaces
.SH SYNOPSIS
@@ -29,7 +29,7 @@ coq-interface (the same as coqtop).
.BR coqc (1),
.BR coqdep (1),
.BR coqtop (1),
-.BR parser (1).
+.BR coq\-parser (1).
.br
.I
The Coq Reference Manual.
diff --git a/man/parser.1 b/man/coq-parser.1
index d89465d8..23dc8201 100644
--- a/man/parser.1
+++ b/man/coq-parser.1
@@ -1,11 +1,11 @@
.TH COQ 1 "April 25, 2001"
.SH NAME
-parser \- Coq parser
+coq\-parser \- Coq parser
.SH SYNOPSIS
-.B parser
+.B coq\-parser
[
.B options
]
@@ -19,7 +19,7 @@ program is not for the casual user.
.SH SEE ALSO
-.BR coq-interface (1),
+.BR coq\-interface (1),
.BR coqc (1),
.BR coqtop (1),
.BR coqdep (1).
diff --git a/man/coq-tex.1 b/man/coq-tex.1
index 737de70a..7e0a2f81 100644
--- a/man/coq-tex.1
+++ b/man/coq-tex.1
@@ -15,19 +15,19 @@ coq-tex \- Process Coq phrases embedded in LaTeX files
.BI \-image \ coq-image
]
[
-.B -w
+.B \-w
]
[
-.B -v
+.B \-v
]
[
-.B -sl
+.B \-sl
]
[
-.B -hrule
+.B \-hrule
]
[
-.B -small
+.B \-small
]
.I input-file ...
@@ -75,7 +75,7 @@ typewriter font.
.TP
.BI \-o \ output-file
Specify the name of a file where the LaTeX output is to be stored. A
-dash `-' causes the LaTeX output to be printed on standard output.
+dash `\-' causes the LaTeX output to be printed on standard output.
.TP
.BI \-n \ line-width
Set the line width. The default is 72 characters. The responses of the
@@ -90,23 +90,23 @@ this is the command
.IR coqtop
without specifying any path which is used to evaluate the Coq phrases.
.TP
-.B -w
+.B \-w
Cause lines to be folded on a space character whenever possible,
avoiding word cuts in the output. By default, folding occurs at
the line width, regardless of word cuts.
.TP
-.B -v
+.B \-v
Verbose mode. Prints the Coq answers on the standard output.
Useful to detect errors in Coq phrases.
.TP
-.B -sl
+.B \-sl
Slanted mode. The Coq answers are written in a slanted font.
.TP
-.B -hrule
+.B \-hrule
Horizontal lines mode. The Coq parts are written between two
horizontal lines.
.TP
-.B -small
+.B \-small
Small font mode. The Coq parts are written in a smaller font.
diff --git a/man/coqdep.1 b/man/coqdep.1
index 6ae89f8b..e2cbb40e 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -67,7 +67,7 @@ Prints a warning if a Coq command
.IR Module \&
is incorrect. (For instance, you wrote `Declare ML Module "A".',
but the module A contains #open "B"). The correct command is printed
-(see option -D). The warning is printed on standard error.
+(see option \-D). The warning is printed on standard error.
.TP
.BI \-i
Prints also the dependencies for .vi files (Coq specification modules).
@@ -138,7 +138,7 @@ Z.v contains the commands `Require X' and `Declare ML Module "D"'.
To get the dependencies of the Coq files:
.IP
.B
-example% coqdep -I . *.v
+example% coqdep \-I . *.v
.RS
.sp .5
.nf
@@ -153,7 +153,7 @@ example% coqdep -I . *.v
With a warning:
.IP
.B
-example% coqdep -w -I . *.v
+example% coqdep \-w \-I . *.v
.RS
.sp .5
.nf
@@ -170,7 +170,7 @@ example% coqdep -w -I . *.v
To get only the Caml dependencies:
.IP
.B
-example% coqdep -c -I . *.ml
+example% coqdep \-c \-I . *.ml
.RS
.sp .5
.nf
@@ -190,4 +190,4 @@ example% coqdep -c -I . *.ml
.SH BUGS
Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index c443e8b0..45fcafd2 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -54,7 +54,7 @@ Redirect the output into the file
Output files into directory
.I dir
instead of current directory (option
--d does not change the filename specified with option -o, if any).
+\-d does not change the filename specified with option \-o, if any).
.TP
.B \-s, \ \-\-short
Do not insert titles for the files. The default behavior is to insert
@@ -68,7 +68,7 @@ Suppress the header and trailer of the final document. Thus, you can
insert the resulting document into a larger one.
.TP
.BI \-p \ string, \ \-\-preamble \ string
-Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with -html).
+Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
.TP
.BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
Considers the file `file' respectively as a .v (or .g) file or a .tex file.
@@ -114,7 +114,7 @@ it builds a table of contents into toc.html.
.TP
.B \-\-glob\-from \ file
Make references using Coq globalizations from file file. (Such
-globalizations are obtained with Coq option -dump-glob).
+globalizations are obtained with Coq option \-dump\-glob).
.TP
.B \-\-no\-externals
@@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar
Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
.TP
-.BI -R \ dir \ coqdir
+.BI \-R \ dir \ coqdir
Map physical directory dir to Coq logical directory coqdir (similarly
-to Coq option -R).
+to Coq option \-R).
.B Note:
-option -R only has effect on the files following it on the command
+option \-R only has effect on the files following it on the command
line, so you will probably need to put this option first.
.SS Contents options
.TP
-.B -g, \ --gallina
+.B \-g, \ \-\-gallina
Do not print proofs.
.TP
-.B -l, \ --light
-Light mode. Suppress proofs (as with -g) and the following commands:
+.B \-l, \ \-\-light
+Light mode. Suppress proofs (as with \-g) and the following commands:
* [Recursive] Tactic Definition
* Hint / Hints
@@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands:
* Implicit Argument / Implicits
* Section / Variable / Hypothesis / End
-The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
+The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
.SS Language options
Default behavior is to assume ASCII 7 bits input files.
.TP
-.B -latin1, \ --latin1
-Select ISO-8859-1 input files. It is equivalent to --inputenc latin1
---charset iso-8859-1.
+.B \-latin1, \ \-\-latin1
+Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
+\-\-charset iso\-8859\-1.
.TP
-.B -utf8, \ --utf8
-Select UTF-8 (Unicode) input files. It is equivalent to --inputenc
-utf8 --charset utf-8. LATEX UTF-8 support can be found at
-http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
+.B \-utf8, \ \-\-utf8
+Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
+utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
+http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
.TP
-.BI --inputenc \ string
+.BI \-\-inputenc \ string
Give a LATEX input encoding, as an option to LATEX package inputenc.
.TP
-.BI --charset \ string
+.BI \-\-charset \ string
Specify the HTML character set, to be inserted in the HTML header.
diff --git a/man/coqide.1 b/man/coqide.1
new file mode 100644
index 00000000..20379ef4
--- /dev/null
+++ b/man/coqide.1
@@ -0,0 +1,166 @@
+.TH COQIDE 1 "July 16, 2004"
+
+.SH NAME
+coqide \- The Coq Proof Assistant graphical interface
+
+
+.SH SYNOPSIS
+.B coqide
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is a gtk graphical interface for the Coq proof assistant.
+
+For command-line-oriented use of Coq, see
+.BR coqide (1)
+; for batch-oriented use of Coq, see
+.BR coqc (1).
+
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Show the complete list of options accepted by
+.BR coqide .
+.TP
+.BI \-I\ dir ,\ \-include\ dir
+Add directory dir in the include path.
+.TP
+.BI \-R\ dir\ coqdir
+Recursively map physical
+.I dir
+to logical
+.IR coqdir .
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.BI \-is\ f ,\ \-inputstate\ f
+Read state from
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\ f
+Write state in file
+.IR f .coq.
+.TP
+.BI \-load\-ml\-object\ f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\ f
+Load ML file
+.IR f .
+.TP
+.BI \-l\ f ,\ \-load\-vernac\-source\ f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\ f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\ f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.TP
+.BI \-compile\ f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\ f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR -batch ).
+.TP
+.B \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B -v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\ f
+Set the rcfile to
+.IR f .
+.TP
+.BI \-user\ u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\ f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coqtop (1),
+.BR coq-tex (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual,
+.I
+The Coq web site: http://coq.inria.fr,
+.I
+/usr/share/doc/coqide/FAQ.
+
+.SH AUTHOR
+This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
+for the Debian project (but may be used by others).
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index 3640d439..1b9c9e2a 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -17,10 +17,10 @@ coqmktop \- The Coq Proof Assistant user-tactics linker
.B coqmktop
builds a new Coq toplevel extended with user-tactics.
.IR files \&
-are the Objective Caml object or library files (i.e. with suffix .cmo,
-.cmx, .cma or .cmxa) to link with the Coq system.
+are the Objective Caml object or library files
+(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system.
The linker produces an executable Coq toplevel which can be called
-directly or through coqc(1), using the -image option.
+directly or through coqc(1), using the \-image option.
.SH OPTIONS
diff --git a/man/coqwc.1 b/man/coqwc.1
index 7011d148..4594aeec 100644
--- a/man/coqwc.1
+++ b/man/coqwc.1
@@ -44,4 +44,4 @@ Do not skip headers
.SH BUGS
Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3aa51c53..4811c443 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
* on May-June 2006 for implementation of abstraction of pretty-printing of objects.
*)
-(* $Id: prettyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: prettyp.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Pp
open Util
@@ -744,7 +744,7 @@ let print_path_between cls clt =
let j = index_of_class clt in
let p =
try
- lookup_path_between (i,j)
+ lookup_path_between_class (i,j)
with _ ->
errorlabstrm "index_cl_of_id"
(str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 0bdae7c7..be73f573 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -60,10 +60,10 @@ let rec print_module name locals with_body mb =
in
let modtype = match mb.mod_type with
None -> str ""
- | Some t -> str": " ++
+ | Some t -> spc () ++ str": " ++
print_modtype locals t
in
- hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body)
+ hv 2 (str "Module " ++ name ++ modtype ++ body)
and print_modtype locals mty =
match mty with
@@ -102,7 +102,7 @@ and print_sig locals msid sign =
| SFBconst {const_opaque=true} -> str "Parameter "
| SFBmind _ -> str "Inductive "
| SFBmodule _ -> str "Module "
- | SFBalias (mp,_) -> str "Module"
+ | SFBalias (mp,_) -> str "Module "
| SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
in
prlist_with_sep spc print_spec sign
@@ -114,7 +114,7 @@ and print_struct locals msid struc =
| SFBconst {const_body=None} -> str "Parameter "
| SFBmind _ -> str "Inductive "
| SFBmodule _ -> str "Module "
- | SFBalias (mp,_) -> str "Module"
+ | SFBalias (mp,_) -> str "Module "
| SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
in
prlist_with_sep spc print_body struc
@@ -125,9 +125,9 @@ and print_modexpr locals mexpr = match mexpr with
(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env
in *)
let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
- hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++
+ hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
str ":" ++ print_modtype locals mty.typ_expr ++
- str "]" ++ spc () ++ print_modexpr locals' mexpr)
+ str ")" ++ spc () ++ print_modexpr locals' mexpr)
| SEBstruct (msid, struc) ->
hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
| SEBapply (mexpr,marg,_) ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b5a5709e..398da529 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: classops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Util
open Pp
@@ -128,6 +128,10 @@ let class_exists cl = Bijint.mem cl !class_tab
let class_info_from_index i = Bijint.map i !class_tab
+let cl_fun_index = fst(class_info CL_FUN)
+
+let cl_sort_index = fst(class_info CL_SORT)
+
(* coercion_info : coe_typ -> coe_info_typ *)
let coercion_info coe = Gmap.find coe !coercion_tab
@@ -136,32 +140,10 @@ let coercion_exists coe = Gmap.mem coe !coercion_tab
let coercion_params coe_info = coe_info.coe_param
-let lookup_path_between (s,t) =
- Gmap.find (s,t) !inheritance_graph
-
-let lookup_path_to_fun_from s =
- lookup_path_between (s,fst(class_info CL_FUN))
+(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
-let lookup_path_to_sort_from s =
- lookup_path_between (s,fst(class_info CL_SORT))
-
-let lookup_pattern_path_between (s,t) =
- let l = Gmap.find (s,t) !inheritance_graph in
- List.map
- (fun coe ->
- let c, _ =
- Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty
- coe.coe_value
- in
- match kind_of_term c with
- | Construct cstr ->
- (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
- | _ -> raise Not_found) l
-
-(* find_class_type : constr -> cl_typ * int *)
-
-let find_class_type t =
- let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in
+let find_class_type env sigma t =
+ let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
match kind_of_term t' with
| Var id -> CL_SECVAR id, args
| Const sp -> CL_CONST sp, args
@@ -178,7 +160,7 @@ let subst_cl_typ subst ct = match ct with
| CL_CONST kn ->
let kn',t = subst_con subst kn in
if kn' == kn then ct else
- fst (find_class_type t)
+ fst (find_class_type (Global.env()) Evd.empty t)
| CL_IND (kn,i) ->
let kn' = subst_kn subst kn in
if kn' == kn then ct else
@@ -188,19 +170,17 @@ let subst_cl_typ subst ct = match ct with
to declare any term as a coercion *)
let subst_coe_typ subst t = fst (subst_global subst t)
-(* classe d'un terme *)
-
(* class_of : Term.constr -> int *)
let class_of env sigma t =
let (t, n1, i, args) =
try
- let (cl,args) = find_class_type t in
+ let (cl,args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, args)
with Not_found ->
let t = Tacred.hnf_constr env sigma t in
- let (cl, args) = find_class_type t in
+ let (cl, args) = find_class_type env sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, args)
in
@@ -208,7 +188,7 @@ let class_of env sigma t =
let inductive_class_of ind = fst (class_info (CL_IND ind))
-let class_args_of c = snd (find_class_type c)
+let class_args_of env sigma c = snd (find_class_type env sigma c)
let string_of_class = function
| CL_FUN -> "Funclass"
@@ -222,6 +202,61 @@ let string_of_class = function
let pr_class x = str (string_of_class x)
+(* lookup paths *)
+
+let lookup_path_between_class (s,t) =
+ Gmap.find (s,t) !inheritance_graph
+
+let lookup_path_to_fun_from_class s =
+ lookup_path_between_class (s,cl_fun_index)
+
+let lookup_path_to_sort_from_class s =
+ lookup_path_between_class (s,cl_sort_index)
+
+(* advanced path lookup *)
+
+let apply_on_class_of env sigma t cont =
+ try
+ let (cl,args) = find_class_type env sigma t in
+ let (i, { cl_param = n1 } ) = class_info cl in
+ if List.length args <> n1 then raise Not_found;
+ t, cont i
+ with Not_found ->
+ (* Is it worth to be more incremental on the delta steps? *)
+ let t = Tacred.hnf_constr env sigma t in
+ let (cl, args) = find_class_type env sigma t in
+ let (i, { cl_param = n1 } ) = class_info cl in
+ if List.length args <> n1 then raise Not_found;
+ t, cont i
+
+let lookup_path_between env sigma (s,t) =
+ let (s,(t,p)) =
+ apply_on_class_of env sigma s (fun i ->
+ apply_on_class_of env sigma t (fun j ->
+ lookup_path_between_class (i,j))) in
+ (s,t,p)
+
+let lookup_path_to_fun_from env sigma s =
+ apply_on_class_of env sigma s lookup_path_to_fun_from_class
+
+let lookup_path_to_sort_from env sigma s =
+ apply_on_class_of env sigma s lookup_path_to_sort_from_class
+
+let get_coercion_constructor coe =
+ let c, _ =
+ Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value
+ in
+ match kind_of_term c with
+ | Construct cstr ->
+ (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
+ | _ ->
+ raise Not_found
+
+let lookup_pattern_path_between (s,t) =
+ let i = inductive_class_of s in
+ let j = inductive_class_of t in
+ List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph)
+
(* coercion_value : coe_index -> unsafe_judgment * bool *)
let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
@@ -255,11 +290,11 @@ let add_coercion_in_graph (ic,source,target) =
try
if i=j then begin
if different_class_params i j then begin
- let _ = lookup_path_between ij in
+ let _ = lookup_path_between_class ij in
ambig_paths := (ij,p)::!ambig_paths
end
end else begin
- let _ = lookup_path_between (i,j) in
+ let _ = lookup_path_between_class (i,j) in
ambig_paths := (ij,p)::!ambig_paths
end;
false
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 1436a11b..a76fe75c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: classops.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: classops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*)
(*i*)
open Names
@@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ)
val class_exists : cl_typ -> bool
val class_info_from_index : cl_index -> cl_typ * cl_info_typ
-(* [find_class_type c] returns the head reference of c and its
+(* [find_class_type env sigma c] returns the head reference of [c] and its
arguments *)
-val find_class_type : constr -> cl_typ * constr list
+val find_class_type : env -> evar_map -> types -> cl_typ * constr list
(* raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> constr -> constr * cl_index
+val class_of : env -> evar_map -> types -> types * cl_index
(* raises [Not_found] if not mapped to a class *)
val inductive_class_of : inductive -> cl_index
-val class_args_of : constr -> constr list
+val class_args_of : env -> evar_map -> types -> constr list
(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
val declare_coercion :
@@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool
val coercion_value : coe_index -> (unsafe_judgment * bool)
(*s Lookup functions for coercion paths *)
-val lookup_path_between : cl_index * cl_index -> inheritance_path
-val lookup_path_to_fun_from : cl_index -> inheritance_path
-val lookup_path_to_sort_from : cl_index -> inheritance_path
-val lookup_pattern_path_between :
- cl_index * cl_index -> (constructor * int) list
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+
+val lookup_path_between : env -> evar_map -> types * types ->
+ types * types * inheritance_path
+val lookup_path_to_fun_from : env -> evar_map -> types ->
+ types * inheritance_path
+val lookup_path_to_sort_from : env -> evar_map -> types ->
+ types * inheritance_path
+val lookup_pattern_path_between :
+ inductive * inductive -> (constructor * int) list
(*i Crade *)
open Pp
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3074c4c4..73fcd0ea 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Util
open Names
@@ -78,10 +78,6 @@ module Default = struct
| App (f,l) -> mkApp (whd_evar sigma f,l)
| _ -> whd_evar sigma t
- let class_of1 env evd t =
- let sigma = evars_of evd in
- class_of env sigma (whd_app_evar sigma t)
-
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env argl funj =
let rec apply_rec acc typ = function
@@ -107,18 +103,16 @@ module Default = struct
(* raise Not_found if no coercion found *)
let inh_pattern_coerce_to loc pat ind1 ind2 =
- let i1 = inductive_class_of ind1 in
- let i2 = inductive_class_of ind2 in
- let p = lookup_pattern_path_between (i1,i2) in
+ let p = lookup_pattern_path_between (ind1,ind2) in
apply_pattern_coercion loc pat p
(* appliquer le chemin de coercions p à hj *)
- let apply_coercion env p hj typ_cl =
+ let apply_coercion env sigma p hj typ_cl =
try
fst (List.fold_left
(fun (ja,typ_cl) i ->
let fv,isid = coercion_value i in
- let argl = (class_args_of typ_cl)@[ja.uj_val] in
+ let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
let jres = apply_coercion_args env argl fv in
(if isid then
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -137,16 +131,15 @@ module Default = struct
(evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
(try
- let t,i1 = class_of1 env evd j.uj_type in
- let p = lookup_path_to_fun_from i1 in
- (evd,apply_coercion env p j t)
+ let t,p =
+ lookup_path_to_fun_from env (evars_of evd) j.uj_type in
+ (evd,apply_coercion env (evars_of evd) p j t)
with Not_found -> (evd,j))
let inh_tosort_force loc env evd j =
try
- let t,i1 = class_of1 env evd j.uj_type in
- let p = lookup_path_to_sort_from i1 in
- let j1 = apply_coercion env p j t in
+ let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
+ let j1 = apply_coercion env (evars_of evd) p j t in
let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
(evd,type_judgment env j2)
with Not_found ->
@@ -173,12 +166,12 @@ module Default = struct
else
let v', t' =
try
- let t1,i1 = class_of1 env evd c1 in
- let t2,i2 = class_of1 env evd t in
- let p = lookup_path_between (i2,i1) in
+ let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
match v with
Some v ->
- let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+ let j =
+ apply_coercion env (evars_of evd) p
+ {uj_val = v; uj_type = t} t2 in
Some j.uj_val, j.uj_type
| None -> None, t
with Not_found -> raise NoCoercion
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2f507318..21e881b9 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reductionops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Pp
open Util
@@ -233,6 +233,7 @@ let evar = mkflags [fevar]
let betaevar = mkflags [fevar; fbeta]
let betaiota = mkflags [fiota; fbeta]
let betaiotazeta = mkflags [fiota; fbeta;fzeta]
+let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar]
(* Contextual *)
let delta = mkflags [fdelta;fevar]
@@ -483,6 +484,12 @@ let whd_betaiotazeta_stack x =
let whd_betaiotazeta x =
app_stack (whd_betaiotazeta_state (x, empty_stack))
+let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar
+let whd_betaiotazetaevar_stack env sigma x =
+ appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+let whd_betaiotazetaevar env sigma x =
+ app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+
let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
let whd_betaiotaevar_stack env sigma x =
appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1ac36b2a..c026d9fe 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reductionops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*)
(*i*)
open Names
@@ -98,6 +98,7 @@ val whd_evar : evar_map -> constr -> constr
val whd_beta : local_reduction_function
val whd_betaiota : local_reduction_function
val whd_betaiotazeta : local_reduction_function
+val whd_betaiotazetaevar : contextual_reduction_function
val whd_betadeltaiota : contextual_reduction_function
val whd_betadeltaiota_nolet : contextual_reduction_function
val whd_betaetalet : local_reduction_function
@@ -105,17 +106,17 @@ val whd_betalet : local_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack : contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
+val whd_betaiotazetaevar_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
val whd_betaetalet_stack : local_stack_reduction_function
val whd_betalet_stack : local_stack_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state : contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
+val whd_betaiotazetaevar_state : contextual_state_reduction_function
+val whd_betadeltaiota_state : contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
val whd_betaetalet_state : local_state_reduction_function
val whd_betalet_state : local_state_reduction_function
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index e87a195f..2569b292 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqmktop.ml 11260 2008-07-24 20:53:12Z letouzey $ *)
+(* $Id: coqmktop.ml 11380 2008-09-07 12:27:27Z glondu $ *)
(* coqmktop is a script to link Coq, analogous to ocamlmktop.
The command line contains options specific to coqmktop, options for the
@@ -289,7 +289,8 @@ let main () =
(* bytecode (we shunt ocamlmktop script which fails on win32) *)
let ocamlmktoplib = " toplevellib.cma" in
let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
- let ocamlccustom = ocamlcexec^" -custom -linkall" in
+ let ocamlccustom = Printf.sprintf "%s %s -linkall "
+ ocamlcexec Coq_config.coqrunbyteflags in
(if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
in
(* files to link *)
diff --git a/test-suite/check b/test-suite/check
index 571e7a67..47960e98 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -65,7 +65,7 @@ test_output() {
done
}
-# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
+# La fonction suivante teste l'analyseur syntaxique fournit par "coq-parser"
# Elle fonctionne comme test_output
test_parser() {
if [ -d $1 ]; then
@@ -74,7 +74,7 @@ test_parser() {
printf " "$f"..."
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
foutput=`dirname $f`/`basename $f .v`.out
- echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
+ echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1
perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
$tmpoutput 2>&1 | grep -i error > /dev/null
if [ $? = 0 ] ; then
@@ -250,8 +250,16 @@ echo "Interactive tests"
test_interactive interactive
echo "Micromega tests"
test_success micromega
-echo "Complexity tests"
-test_complexity complexity
+
+# We give a chance to disable the complexity tests which may cause
+# random build failures on build farms
+if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then
+ echo "Complexity tests"
+ test_complexity complexity
+else
+ echo "Skipping complexity tests"
+fi
+
echo "Module tests"
$coqtop -compile modules/Nat
$coqtop -compile modules/plik
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index d652132e..525348de 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
End Q.
+(* Combining class lookup and path lookup so that if a lookup fails, another
+ descent in the class can be found (see wish #1934) *)
+
+Record Setoid : Type :=
+{ car :> Type }.
+
+Record Morphism (X Y:Setoid) : Type :=
+{evalMorphism :> X -> Y}.
+
+Definition extSetoid (X Y:Setoid) : Setoid.
+intros X Y.
+constructor.
+exact (Morphism X Y).
+Defined.
+
+Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
+
+Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
+
+Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
+
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 94444f5b..05cd1892 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FMapFacts.v 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: FMapFacts.v 11359 2008-09-04 09:43:36Z notin $ *)
(** * Finite maps library *)
@@ -975,7 +975,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
fold (fun k e b => if f k e then true else b) m false.
Definition partition (f : key -> elt -> bool)(m : t elt) :=
- (filter f m, filter (fun k e => negb (f k e))).
+ (filter f m, filter (fun k e => negb (f k e)) m).
Section Specs.
Variable f : key -> elt -> bool.
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 3900987e..65c39b7a 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -24,7 +24,8 @@ body { padding: 0px 0px;
#main{ display: block;
padding: 10px;
overflow: hidden;
- font-size: 10pt }
+ font-size: 100%;
+ line-height: 80% }
#main a.idref:visited {color : #416DFF; text-decoration : none; }
#main a.idref:link {color : #416DFF; text-decoration : none; }
@@ -39,16 +40,16 @@ body { padding: 0px 0px;
#main .keyword { color : #cf1d1d }
#main { color: black }
-#main .section { background-color:#899BD6;
- font-size : 20pt }
+#main .section { background-color:#90bdff;
+ font-size : 175% }
-#main code { font-family: monospace;
- line-height: 50% }
+#main code { font-family: monospace }
#main .doc { margin: 0px;
padding: 10px;
font-family: sans-serif;
- font-size: 11pt;
+ font-size: 100%;
+ line-height: 100%;
font-weight:bold;
color: black;
background-color: #90bdff;
@@ -58,7 +59,7 @@ body { padding: 0px 0px;
/* Pied de page */
-#footer { font-size: 8pt;
+#footer { font-size: 65%;
font-family: sans-serif; }
#footer a:visited { color: blue; }
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 2c6a63b0..6ebc663b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
open Util
open Pp
@@ -139,7 +139,7 @@ let get_source lp source =
let (cl1,lv1) =
match lp with
| [] -> raise Not_found
- | t1::_ -> find_class_type t1
+ | t1::_ -> find_class_type (Global.env()) Evd.empty t1
in
(cl1,lv1,1)
| Some cl ->
@@ -147,7 +147,7 @@ let get_source lp source =
| [] -> raise Not_found
| t1::lt ->
try
- let cl1,lv1 = find_class_type t1 in
+ let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
if cl = cl1 then cl1,lv1,(List.length lt+1)
else raise Not_found
with Not_found -> aux lt
@@ -157,7 +157,7 @@ let get_target t ind =
if (ind > 1) then
CL_FUN
else
- fst (find_class_type t)
+ fst (find_class_type (Global.env()) Evd.empty t)
let prods_of t =
let rec aux acc d = match kind_of_term d with
@@ -225,8 +225,9 @@ let build_id_coercion idf_opt source =
match idf_opt with
| Some idf -> idf
| None ->
+ let cl,_ = find_class_type (Global.env()) Evd.empty t in
id_of_string ("Id_"^(ident_key_of_class source)^"_"^
- (ident_key_of_class (fst (find_class_type t))))
+ (ident_key_of_class cl))
in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry