diff --git a/.gitignore b/.gitignore
index 7fcd258..32a40af 100644
--- a/.gitignore
+++ b/.gitignore
@@ -79,6 +79,9 @@
doc/stdlib/Library.pdf
doc/stdlib/Library.ps
doc/stdlib/Library.coqdoc.tex
+doc/stdlib/FullLibrary.pdf
+doc/stdlib/FullLibrary.ps
+doc/stdlib/FullLibrary.coqdoc.tex
doc/stdlib/html/
doc/stdlib/index-body.html
doc/stdlib/index-list.html
diff --git a/CHANGES b/CHANGES
index 74aefe4..c245fb2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,54 @@
-Changes from V8.3 to V8.4
-=========================
+Changes from V8.4beta to V8.4
+=============================
+
+Vernacular commands
+
+- Undo and UndoTo are now handling the proof states. They may
+ perform some extra steps of backtrack to avoid states where
+ the proof state is unavailable (typically a closed proof).
+- The commands Suspend and Resume have been removed.
+- A basic Show Script has been reintroduced (no indentation).
+- New command "Set Parsing Explicit" for deactivating parsing (and printing)
+ of implicit arguments (useful for teaching).
+- New command "Grab Existential Variables" to transform the unresolved evars at
+ the end of a proof into goals.
+
+Tactics
+
+- Still no general "info" tactical, but new specific tactics
+ info_auto, info_eauto, info_trivial which provides information
+ on the proofs found by auto/eauto/trivial. Display of these
+ details could also be activated by Set Info Auto/Eauto/Trivial.
+- Details on everything tried by auto/eauto/trivial during
+ a proof search could be obtained by "debug auto", "debug eauto",
+ "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
+- New command "r string" that interprets "idtac string" as a breakpoint
+ and jumps to its next use in Ltac debugger.
+- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
+ harvey, zenon, gwhy) have been removed, since Why2 has not been
+ maintained for the last few years. The Why3 plugin should be a suitable
+ replacement in most cases.
+
+Libraries
+
+- MSetRBT : a new implementation of MSets via Red-Black trees (initial
+ contribution by Andrew Appel).
+- MSetAVL : for maximal sharing with the new MSetRBT, the argument order
+ of Node has changed (this should be transparent to regular MSets users).
+
+Module System
+
+- The names of modules (and module types) are now in a fully separated
+ namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+ is now accepted.
+
+CoqIDE
+
+- Coqide now supports the Restart command, and Undo (with a warning).
+ Better support for Abort.
+
+Changes from V8.3 to V8.4beta
+=============================
Logic
@@ -69,6 +118,8 @@
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
+- The behavior of the simpl tactic can be tuned using the new "Arguments"
+ vernacular.
Vernacular commands
@@ -90,6 +141,7 @@
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
+- New command "Arguments" subsuming "Implicit Arguments" and "Arguments Scope".
Module System
diff --git a/COPYRIGHT b/COPYRIGHT
index 8d81d8c..3aa6aae 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,6 +1,6 @@
The Coq proof assistant
-Copyright 1999-2010 The Coq development team, INRIA, CNRS, University
+Copyright 1999-2012 The Coq development team, INRIA, CNRS, University
Paris Sud, University Paris 7, Ecole Polytechnique.
This product includes also software developed by
diff --git a/CREDITS b/CREDITS
index 53bd9e9..543cb3f 100644
--- a/CREDITS
+++ b/CREDITS
@@ -106,6 +106,7 @@
of the Coq Proof assistant during the indicated time:
Bruno Barras (INRIA, 1995-now)
+ Pierre Boutillier (INRIA-PPS, 2010-now)
Jacek Chrzaszcz (LRI, 1998-2003)
Thierry Coquand (INRIA, 1985-1989)
Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-now)
@@ -118,10 +119,12 @@
Amy Felty (INRIA, 1993)
Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-now)
Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
+ Stéphane Glondu (INRIA-PPS, 2007-now)
Benjamin Grégoire (INRIA, 2003-now)
Hugo Herbelin (INRIA, 1996-now)
Gérard Huet (INRIA, 1985-1997)
- Pierre Letouzey (LRI, 2000-2004 & PPS, 2005-now)
+ Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
+ Patrick Loiseleur (Paris Sud, 1997-1999)
Evgeny Makarov (INRIA, 2007)
Pascal Manoury (INRIA, 1993)
Micaela Mayero (INRIA, 1997-2002)
@@ -132,9 +135,11 @@
Julien Narboux (INRIA, 2005-2006, Strasbourg, 2007-now)
Jean-Marc Notin (CNRS, 2006-now)
Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
- Patrick Loiseleur (Paris Sud, 1997-1999)
Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997,
LRI, 1997-now)
+ Pierre-Marie Pédrot (INRIA-PPS, 2011-now)
+ Matthias Puech (INRIA-Bologna, 2008-now)
+ Yann Régis-Gianas (INRIA-PPS, 2009-now)
Clément Renard (INRIA, 2001-2004)
Claudio Sacerdoti Coen (INRIA, 2004-2005)
Amokrane Saïbi (INRIA, 1993-1998)
@@ -142,6 +147,7 @@
Élie Soubiran (INRIA, 2007-now)
Matthieu Sozeau (INRIA, 2005-now)
Arnaud Spiwack (INRIA, 2006-now)
+ Enrico Tassi (INRIA, 2011-now)
Benjamin Werner (INRIA, 1989-1994)
***************************************************************************
diff --git a/INSTALL b/INSTALL
index e88dc31..5ee0061 100644
--- a/INSTALL
+++ b/INSTALL
@@ -39,9 +39,9 @@
urpmi coq
- Should you need or prefer to compile Coq V8.2 yourself, you need:
-
- - Objective Caml version 3.10.0 or later
+ Should you need or prefer to compile Coq V8.4 yourself, you need:
+
+ - Objective Caml version 3.11.2 or later
(available at http://caml.inria.fr/)
- Camlp5 (version <= 4.08, or 5.* transitional)
@@ -87,7 +87,7 @@
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
=================================================
-1- Check that you have the Objective Caml compiler version 3.10.0 (or later)
+1- Check that you have the Objective Caml compiler version 3.11.2 (or later)
installed on your computer and that "ocamlmktop" and "ocamlc" (or
its native code version "ocamlc.opt") lie in a directory which is present
in your $PATH environment variable.
diff --git a/Makefile b/Makefile
index 876ac58..0ff7285 100644
--- a/Makefile
+++ b/Makefile
@@ -191,6 +191,7 @@
rm -f doc/common/version.tex
rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html
rm -f doc/coq.tex
+ rm -f doc/refman/styles.hva doc/refman/cover.html
archclean: clean-ide optclean voclean
rm -rf _build myocamlbuild_config.ml
@@ -221,7 +222,6 @@
rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
distclean: clean cleanconfig
- $(MAKE) -C test-suite distclean
voclean:
rm -f states/*.coq
diff --git a/Makefile.build b/Makefile.build
index 59ee457..41dfabb 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -318,7 +318,7 @@
$(STRIP) $@
$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
- $(SHOW)'OCAMLOPT -o $@'
+ $(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\
str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
@@ -446,7 +446,7 @@
# 3) plugins
###########################################################################
-.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction
+.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction
.PHONY: field fourier funind cc subtac rtauto pluginsopt
plugins: $(PLUGINSVO)
@@ -455,7 +455,6 @@
ring: $(RINGVO) $(RINGCMA)
setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
nsatz: $(NSATZVO) $(NSATZCMA)
-dp: $(DPCMA)
xml: $(XMLVO) $(XMLCMA)
extraction: $(EXTRACTIONCMA)
field: $(FIELDVO) $(FIELDCMA)
@@ -623,7 +622,7 @@
install-library:
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT)
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
$(MKDIR) $(FULLCOQLIB)/user-contrib
@@ -632,7 +631,7 @@
$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
ifeq ($(BEST),opt)
$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
+ $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
@@ -643,11 +642,14 @@
install-library-light:
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT)
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS)
$(MKDIR) $(FULLCOQLIB)/states
$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
rm -f $(FULLCOQLIB)/revision
-$(INSTALLLIB) revision $(FULLCOQLIB)
+ifeq ($(BEST),opt)
+ $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT)
+endif
install-coq-info: install-coq-manpages install-emacs install-latex
diff --git a/Makefile.common b/Makefile.common
index b560bae..3740b52 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -79,7 +79,7 @@
pretyping interp toplevel/utils toplevel parsing \
ide/utils ide \
$(addprefix plugins/, \
- omega romega micromega quote ring dp \
+ omega romega micromega quote ring \
setoid_ring xml extraction fourier \
cc funind firstorder field subtac \
rtauto nsatz syntax decl_mode)
@@ -125,14 +125,15 @@
RefMan-cic.v.tex RefMan-lib.v.tex \
RefMan-tacex.v.tex RefMan-syn.v.tex \
RefMan-oth.v.tex RefMan-ltac.v.tex \
- RefMan-decl.v.tex \
+ RefMan-decl.v.tex RefMan-sch.v.tex \
+ RefMan-pro.v.tex \
Cases.v.tex Coercion.v.tex Extraction.v.tex \
Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
Setoid.v.tex Helm.tex Classes.v.tex )
REFMANTEXFILES:=$(addprefix doc/refman/, \
headers.sty Reference-Manual.tex \
- RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \
+ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \
$(REFMANCOQTEXFILES) \
@@ -176,7 +177,6 @@
RINGCMA:=plugins/ring/ring_plugin.cma
NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-DPCMA:=plugins/dp/dp_plugin.cma
FIELDCMA:=plugins/field/field_plugin.cma
XMLCMA:=plugins/xml/xml_plugin.cma
FOURIERCMA:=plugins/fourier/fourier_plugin.cma
@@ -196,14 +196,14 @@
DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
- $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
+ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
$(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
$(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
$(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
ifneq ($(HASNATDYNLINK),false)
STATICPLUGINS:=
- INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
+ INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \
$(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) $(NATSYNTAXCMA)
INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs)
PLUGINS:=$(PLUGINSCMA)
@@ -314,7 +314,6 @@
NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
-DPVO:=$(call cat_vo_itarget, plugins/dp)
RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
XMLVO:=
@@ -322,7 +321,7 @@
PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
$(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
- $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
+ $(RTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \
$(NSATZVO) $(EXTRACTIONVO)
ALLVO:= $(THEORIESVO) $(PLUGINSVO)
@@ -347,8 +346,6 @@
man/coqwc.1 man/coqdoc.1 man/coqide.1 \
man/coq_makefile.1 man/coqmktop.1 man/coqchk.1
-DATE=$(shell LANG=C date +"%B %Y")
-
###########################################################################
# Source documentation
###########################################################################
diff --git a/Makefile.doc b/Makefile.doc
index 59eb2fe..685887f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -12,7 +12,7 @@
######################################################################
.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial
-.PHONY: stdlib full-stdlib faq rectutorial
+.PHONY: stdlib full-stdlib faq rectutorial refman-html-dir
INDEXURLS:=doc/refman/html/index_urls.txt
@@ -126,14 +126,16 @@
INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
ALLINDEXES:= doc/refman/html/index.html $(INDEXES)
-$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+$(ALLINDEXES): refman-html-dir
+
+refman-html-dir: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
- rm -rf doc/refman/html
$(MKDIR) doc/refman/html
$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
(cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
- $(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
+ -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
refman-quick:
(cd doc/refman;\
@@ -200,40 +202,32 @@
### Standard library (browsable html format)
ifdef QUICK
-doc/stdlib/index-body.html:
+doc/stdlib/html/genindex.html:
+else
+doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
+endif
- rm -rf doc/stdlib/html
$(MKDIR) doc/stdlib/html
- $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \
+ $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
-R theories Coq $(THEORIESVO:.vo=.v)
- mv doc/stdlib/html/index.html doc/stdlib/index-body.html
-else
-doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO)
- - rm -rf doc/stdlib/html
- $(MKDIR) doc/stdlib/html
- $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \
- -R theories Coq $(THEORIESVO:.vo=.v)
- mv doc/stdlib/html/index.html doc/stdlib/index-body.html
-endif
+ mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
- ./doc/stdlib/make-library-index doc/stdlib/index-list.html
-
-doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
- cat doc/stdlib/index-list.html > $@
- sed -n -e '/
/,/<\/table>/p' doc/stdlib/index-body.html >> $@
- cat doc/stdlib/index-trailer.html >> $@
+ ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files
+
+doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html
+ cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@
+ cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@
### Standard library (light version, full version is definitely too big)
ifdef QUICK
doc/stdlib/Library.coqdoc.tex:
- $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
else
-doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO)
- $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
+doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
endif
+ $(COQDOC) -q -boot --gallina --body-only --latex --stdout \
+ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
(cd doc/stdlib;\
@@ -255,12 +249,12 @@
doc/stdlib/FullLibrary.coqdoc.tex:
$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-R theories Coq $(THEORIESVO:.vo=.v) > $@
- sed -i "" -e 's///g' $@
+ sed -i.tmp -e 's///g' $@ && rm $@.tmp
else
doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO)
$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-R theories Coq $(THEORIESVO:.vo=.v) > $@
- sed -i "" -e 's///g' $@
+ sed -i.tmp -e 's///g' $@ && rm $@.tmp
endif
doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex
diff --git a/README b/README
index 4f4afa5..9bf63c4 100644
--- a/README
+++ b/README
@@ -38,7 +38,7 @@
discuss questions about the Coq system and related topics. The submission
address is:
- coq-club@coq.inria.fr
+ coq-club@inria.fr
The topics to be discussed in the club should include:
@@ -55,7 +55,7 @@
To be added to, or removed from, the mailing list, please write to:
- coq-club-request@coq.inria.fr
+ coq-club-request@inria.fr
Please use also this address for any questions/suggestions about the
Coq Club. It might sometimes take a few days before your messages get
@@ -67,7 +67,7 @@
Send your bug reports by filling a form at
- http://logical.saclay.inria.fr/coq-bugs
+ http://coq.inria.fr/bugs
To be effective, bug reports should mention the Caml version used
to compile and run Coq, the Coq version (coqtop -v), the configuration
diff --git a/TODO b/TODO
deleted file mode 100644
index d6891e5..0000000
--- a/TODO
+++ /dev/null
@@ -1,53 +0,0 @@
-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 )
-
-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/checker/mod_checking.ml b/checker/mod_checking.ml
index 9942816..e3431fe 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -53,10 +53,14 @@
| SEBident mp -> mp
| _ -> raise Not_path
-let rec list_split_assoc k rev_before = function
+let is_modular = function
+ | SFBmodule _ | SFBmodtype _ -> true
+ | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
| [] -> raise Not_found
- | (k',b)::after when k=k' -> rev_before,b,after
- | h::tail -> list_split_assoc k (h::rev_before) tail
+ | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+ | h::tail -> list_split_assoc km (h::rev_before) tail
let check_definition_sub env cb1 cb2 =
let check_type env t1 t2 =
@@ -131,38 +135,35 @@
let rec check_with env mtb with_decl mp=
match with_decl with
- | With_definition_body _ ->
- check_with_aux_def env mtb with_decl mp;
+ | With_definition_body (idl,c) ->
+ check_with_def env mtb (idl,c) mp;
mtb
- | With_module_body _ ->
- check_with_aux_mod env mtb with_decl mp;
+ | With_module_body (idl,mp1) ->
+ check_with_mod env mtb (idl,mp1) mp;
mtb
-and check_with_aux_def env mtb with_decl mp =
+and check_with_def env mtb (idl,c) mp =
let sig_b = match mtb with
| SEBstruct(sig_b) ->
sig_b
| _ -> error_signature_expected mtb
in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
- id,idl
- | With_definition_body ([],_) | With_module_body ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
let before = List.rev rev_before in
let env' = Modops.add_signature mp before empty_delta_resolver env in
- match with_decl with
- | With_definition_body ([],_) -> assert false
- | With_definition_body ([id],c) ->
+ if idl = [] then
let cb = match spec with
SFBconst cb -> cb
| _ -> error_not_a_constant l
in
check_definition_sub env' c cb
- | With_definition_body (_::_,_) ->
+ else
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
@@ -170,49 +171,36 @@
begin
match old.mod_expr with
| None ->
- let new_with_decl = match with_decl with
- With_definition_body (_,c) ->
- With_definition_body (idl,c)
- | With_module_body (_,c) ->
- With_module_body (idl,c) in
- check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
+ check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_with_incorrect l
-and check_with_aux_mod env mtb with_decl mp =
+and check_with_mod env mtb (idl,mp1) mp =
let sig_b =
match mtb with
| SEBstruct(sig_b) ->
sig_b
| _ -> error_signature_expected mtb in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
- id,idl
- | With_definition_body ([],_) | With_module_body ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in
let before = List.rev rev_before in
- let rec mp_rec = function
- | [] -> mp
- | i::r -> MPdot(mp_rec r,label_of_id i)
- in
let env' = Modops.add_signature mp before empty_delta_resolver env in
- match with_decl with
- | With_module_body ([],_) -> assert false
- | With_module_body ([id], mp1) ->
+ if idl = [] then
let _ = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
in
let (_:module_body) = (lookup_module mp1 env) in ()
- | With_module_body (_::_,mp) ->
+ else
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
@@ -220,17 +208,11 @@
begin
match old.mod_expr with
None ->
- let new_with_decl = match with_decl with
- With_definition_body (_,c) ->
- With_definition_body (idl,c)
- | With_module_body (_,c) ->
- With_module_body (idl,c) in
- check_with_aux_mod env'
- old.mod_type new_with_decl (MPdot(mp,l))
+ check_with_mod env'
+ old.mod_type (idl,mp1) (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_with_incorrect l
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0c97254..9870ba1 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -28,15 +28,18 @@
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
| Module of module_body
| Modtype of module_type_body
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
- let add_nameobjects_of_one j oib map =
- let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+ let ind = make_mind mp empty_dirpath l in
+ let add_mip_nameobjects j oib map =
+ let ip = (ind,j) in
let map =
array_fold_right_i
(fun i id map ->
@@ -46,22 +49,32 @@
in
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
in
- array_fold_right_i add_nameobjects_of_one mib.mind_packets map
-
-
-(* creates namedobject map for the whole signature *)
-
-let make_label_map mp list =
+ array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
+
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
+
+let get_obj mp map l =
+ try Labmap.find l map.objs
+ with Not_found -> error_no_such_label_sub l mp
+
+let get_mod mp map l =
+ try Labmap.find l map.mods
+ with Not_found -> error_no_such_label_sub l mp
+
+let make_labmap mp list =
let add_one (l,e) map =
- let add_map obj = Labmap.add l obj map in
match e with
- | SFBconst cb -> add_map (Constant cb)
- | SFBmind mib ->
- add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
- | SFBmodule mb -> add_map (Module mb)
- | SFBmodtype mtb -> add_map (Modtype mtb)
- in
- List.fold_right add_one list Labmap.empty
+ | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+ | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+ | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+ | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
+ in
+ List.fold_right add_one list empty_labmap
let check_conv_error error f env a1 a2 =
@@ -282,7 +295,6 @@
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv env ty1 ty2
- | _ -> error ()
let rec check_modules env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
@@ -291,29 +303,25 @@
and check_signatures env mp1 sig1 sig2 subst1 subst2 =
- let map1 = make_label_map mp1 sig1 in
+ let map1 = make_labmap mp1 sig1 in
let check_one_body (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l mp1
- in
match spec2 with
| SFBconst cb2 ->
- check_constant env mp1 l info1 cb2 spec2 subst1 subst2
+ check_constant env mp1 l (get_obj mp1 map1 l)
+ cb2 spec2 subst1 subst2
| SFBmind mib2 ->
- check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+ check_inductive env mp1 l (get_obj mp1 map1 l)
+ mib2 spec2 subst1 subst2
| SFBmodule msb2 ->
begin
- match info1 with
+ match get_mod mp1 map1 l with
| Module msb -> check_modules env msb msb2
subst1 subst2
| _ -> error_not_match l spec2
end
| SFBmodtype mtb2 ->
let mtb1 =
- match info1 with
+ match get_mod mp1 map1 l with
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
in
diff --git a/configure b/configure
index 867ee93..44170b9 100755
--- a/configure
+++ b/configure
@@ -6,10 +6,10 @@
#
##################################
-VERSION=8.4beta
+VERSION=8.4beta2
VOMAGIC=08400
STATEMAGIC=58400
-DATE="December 2011"
+DATE=`LC_ALL=C LANG=C date +"%B %Y"`
# Create the bin/ directory if non-existent
test -d bin || mkdir bin
@@ -292,7 +292,7 @@
"") echo "I can't find the program \"date\" in your path."
echo "Please give me the current date"
read COMPILEDATE;;
- *) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
+ *) COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;;
esac
# Architecture
@@ -388,7 +388,7 @@
if [ "$browser_spec" = "no" ]; then
case $ARCH in
- win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
+ win32) BROWSER='start %s' ;;
Darwin) BROWSER='open %s' ;;
*) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
esac
@@ -445,16 +445,16 @@
CAMLVERSION=`"$bytecamlc" -version`
case $CAMLVERSION in
- 1.*|2.*|3.0*)
+ 1.*|2.*|3.0*|3.10*|3.11.[01])
echo "Your version of Objective-Caml is $CAMLVERSION."
if [ "$force_caml_version" = "yes" ]; then
echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
else
- echo " You need Objective-Caml 3.10.0 or later."
+ echo " You need Objective-Caml 3.11.2 or later."
echo " Configuration script failed!"
exit 1
fi;;
- 3.1*)
+ 3.11.2|3.12*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -742,7 +742,7 @@
bindir_def=${W32PREF}bin
libdir_def=${W32PREF}lib
configdir_def=${W32PREF}config
- datadir_def=${W32PREF}data
+ datadir_def=${W32PREF}share
mandir_def=${W32PREF}man
docdir_def=${W32PREF}doc
emacslib_def=${W32PREF}emacs
@@ -795,10 +795,15 @@
*) LIBDIR_OPTION="None";;
esac
-case $configdir_spec/$local in
- yes/*) CONFIGDIR=$configdir;;
- */true) CONFIGDIR=$COQTOP/ide
- configdir_spec=yes;;
+case $configdir_spec/$prefix_spec/$local in
+ yes/*/*) CONFIGDIR=$configdir;;
+ */yes/*) configdir_spec=yes
+ case $ARCH in
+ win32) CONFIGDIR=$prefix/config;;
+ *) CONFIGDIR=$prefix/etc/xdg/coq;;
+ esac;;
+ */*/true) CONFIGDIR=$COQTOP/ide
+ configdir_spec=yes;;
*) printf "Where should I install the Coqide configuration files [$configdir_def]? "
read CONFIGDIR
case $CONFIGDIR in
diff --git a/dev/base_include b/dev/base_include
index d112596..ad2a3ae 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -123,7 +123,6 @@
open Auto
open Autorewrite
open Contradiction
-open Dhyp
open Eauto
open Elim
open Equality
@@ -199,6 +198,11 @@
let pf_e gl s =
Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
+(* Set usual printing since the global env is available from the tracer *)
+let _ = Constrextern.in_debugger := false
+let _ = Constrextern.set_debug_global_reference_printer
+ (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+
open Toplevel
let go = loop
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 6a42678..40a5a82 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -105,12 +105,12 @@
Dumpglob
Reserve
Impargs
-Constrextern
Syntax_def
Implicit_quantifiers
Smartlocate
Constrintern
Modintern
+Constrextern
Tacexpr
Proof_type
Goal
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 3fc9076..3116cbf 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -487,5 +487,9 @@
[id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)]
(id_of_string ("_"^string_of_int j))
+(* Anticipate that printers can be used from ocamldebug and that
+ pretty-printer should not make calls to the global env since ocamldebug
+ runs in a different process and does not have the proper env at hand *)
+let _ = Constrextern.in_debugger := true
let _ = Constrextern.set_debug_global_reference_printer
(if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html
new file mode 100644
index 0000000..138c302
--- /dev/null
+++ b/doc/common/styles/html/coqremote/footer.html
@@ -0,0 +1,45 @@
+
+
+
+
+
+
+
+
+
+
+
+