summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES47
-rw-r--r--COPYRIGHT18
-rw-r--r--CREDITS19
-rw-r--r--Makefile30
-rw-r--r--Makefile.build6
-rw-r--r--Makefile.common3
-rw-r--r--Makefile.doc28
-rw-r--r--Makefile.stage11
-rw-r--r--checker/safe_typing.ml2
-rw-r--r--config/coq_config.mli6
-rwxr-xr-xconfigure22
-rw-r--r--contrib/interface/depends.ml8
-rw-r--r--contrib/subtac/subtac.ml14
-rw-r--r--contrib/subtac/subtac_cases.ml192
-rw-r--r--contrib/subtac/subtac_classes.ml4
-rw-r--r--contrib/subtac/subtac_command.ml2
-rw-r--r--contrib/subtac/subtac_obligations.ml27
-rw-r--r--contrib/subtac/subtac_obligations.mli5
-rw-r--r--contrib/subtac/subtac_pretyping.ml13
-rw-r--r--contrib/subtac/subtac_pretyping.mli3
-rw-r--r--contrib/subtac/subtac_utils.ml24
-rw-r--r--contrib/subtac/subtac_utils.mli8
-rw-r--r--contrib/xml/proofTree2Xml.ml44
-rw-r--r--dev/base_include6
-rw-r--r--doc/common/styles/html/simple/footer.html (renamed from doc/stdlib/index-trailer.html)0
-rw-r--r--doc/common/styles/html/simple/header.html13
-rw-r--r--doc/common/styles/html/simple/style.css13
-rw-r--r--doc/stdlib/index-list.html.template16
-rw-r--r--ide/coq.ml4
-rw-r--r--ide/coqide.ml8
-rw-r--r--ide/preferences.ml6
-rwxr-xr-xinstall.sh2
-rw-r--r--kernel/environ.ml40
-rw-r--r--kernel/environ.mli9
-rw-r--r--kernel/mod_subst.ml20
-rw-r--r--kernel/modops.ml8
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--lib/util.ml4
-rw-r--r--library/declare.ml6
-rw-r--r--library/declare.mli4
-rw-r--r--library/declaremods.ml90
-rw-r--r--library/impargs.ml56
-rw-r--r--library/impargs.mli4
-rw-r--r--library/lib.ml22
-rw-r--r--library/lib.mli6
-rw-r--r--library/states.ml9
-rw-r--r--library/states.mli7
-rw-r--r--parsing/g_tactic.ml411
-rw-r--r--parsing/g_vernac.ml414
-rw-r--r--parsing/pcoq.ml47
-rw-r--r--parsing/ppvernac.ml5
-rw-r--r--parsing/prettyp.ml7
-rw-r--r--parsing/printer.ml42
-rw-r--r--pretyping/cases.ml29
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evarutil.ml49
-rw-r--r--pretyping/evarutil.mli12
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/recordops.ml7
-rw-r--r--pretyping/termops.ml11
-rw-r--r--pretyping/termops.mli4
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/unification.ml6
-rw-r--r--proofs/clenvtac.ml3
-rw-r--r--proofs/evar_refiner.ml15
-rw-r--r--proofs/evar_refiner.mli7
-rw-r--r--proofs/logic.ml29
-rw-r--r--proofs/proof_type.ml6
-rw-r--r--proofs/proof_type.mli6
-rw-r--r--proofs/tacmach.ml14
-rw-r--r--proofs/tacmach.mli6
-rw-r--r--tactics/auto.ml101
-rw-r--r--tactics/auto.mli3
-rw-r--r--tactics/class_tactics.ml417
-rw-r--r--tactics/decl_proof_instr.ml4
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/evar_tactics.ml8
-rw-r--r--tactics/evar_tactics.mli4
-rw-r--r--tactics/extraargs.ml46
-rw-r--r--tactics/extraargs.mli4
-rw-r--r--tactics/hiddentac.ml6
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/refine.ml27
-rw-r--r--tactics/tacinterp.ml46
-rw-r--r--tactics/tacinterp.mli5
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tactics.ml72
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1905.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2089.v17
-rw-r--r--test-suite/success/dependentind.v3
-rw-r--r--theories/Classes/EquivDec.v15
-rw-r--r--theories/Classes/Equivalence.v8
-rw-r--r--theories/Classes/Init.v11
-rw-r--r--theories/Classes/Morphisms.v50
-rw-r--r--theories/Classes/Morphisms_Relations.v1
-rw-r--r--theories/Classes/RelationClasses.v9
-rw-r--r--theories/Classes/SetoidAxioms.v4
-rw-r--r--theories/Classes/SetoidClass.v4
-rw-r--r--theories/Classes/SetoidTactics.v12
-rw-r--r--theories/FSets/FMapFacts.v4
-rw-r--r--theories/FSets/FSetFacts.v10
-rw-r--r--theories/Logic/ConstructiveEpsilon.v6
-rw-r--r--theories/Logic/FunctionalExtensionality.v2
-rw-r--r--theories/Program/Equality.v10
-rw-r--r--theories/Program/Wf.v12
-rw-r--r--theories/Setoids/Setoid.v4
-rw-r--r--tools/coq_makefile.ml420
-rw-r--r--tools/coqdoc/cdglobals.ml3
-rw-r--r--tools/coqdoc/coqdoc.css33
-rw-r--r--tools/coqdoc/coqdoc.sty3
-rw-r--r--tools/coqdoc/main.ml7
-rw-r--r--tools/coqdoc/output.ml55
-rw-r--r--tools/coqdoc/output.mli5
-rw-r--r--tools/coqdoc/pretty.mll134
-rw-r--r--toplevel/classes.ml26
-rw-r--r--toplevel/command.ml26
-rw-r--r--toplevel/command.mli6
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/vernacentries.ml17
-rw-r--r--toplevel/vernacexpr.ml4
121 files changed, 1125 insertions, 879 deletions
diff --git a/CHANGES b/CHANGES
index 494575fa..4bc0bd82 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,50 @@
+Changes from V8.2 to forthcoming V8.2pl1
+========================================
+
+Language and commands
+
+- Fixing Not_found bug in Theorem with.
+- Fixing pattern parsing bug #2087.
+- Fixing name aliases bug #2085 with modules.
+- Fixing checker bug #2065 with -impredicative-set option.
+- Complying with 8.1 heuristic when unification returns several solutions.
+- Add [Print Opaque Dependencies] command to print the assumptions and
+ the opaque constants a definition uses.
+- Fixing performance issue in Program's type inference when there are
+ many existentials.
+- Fixing bug #2093, using Program does not require to import Program.Tactics
+ anymore, it will use [idtac] as the default obligation tactic.
+- Fix imports when requiring Setoid, to avoid cluttering the context with
+ internal names (possible source of incompatibility, import Morphisms to fix).
+- Fixing bug #2089, Combined Scheme was not treating parameters correctly.
+- Fixing Program to use hooks correctly, when called through [Program Coercion]
+ for example.
+- Fixing manual implicit arguments to always work and remove
+ [Set Manual Implicit Arguments] option (possible source of incompatibility).
+- Fixing refine to work with typeclasses.
+- Fixing implementation of [Context] to discharge class instances only on definitions
+ using some of the parameters or the instance itself (possible source of
+ incompatibility).
+
+Tactics
+
+- Fixing correct binding of quantified hypotheses for induction/destruction
+ when used in Ltac.
+- Fixing bad parentheses check in "pose (f binders := ...)" syntax.
+- Fixing unbalanced parenthesis in Ltac debug trace printer.
+- Fixing missing sort unification check in lemma application (bug #2084).
+- Fixing "as" clause of "apply in" that was not working in the general case.
+- Fixing eauto not using external hints with no pattern.
+
+Tools and development
+
+- Fixing missing -c option in coq_makefile.
+- Temporary hack for coqide.byte "double free or corruption" problem.
+- Added support for code development under Bazaar.
+- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
+- Parsing fixes and support for parsing regular comments inline in coqdoc,
+ using option -parse-comments (suggestions by B. Pierce).
+
Changes from V8.1 to V8.2
=========================
diff --git a/COPYRIGHT b/COPYRIGHT
index 7ed31f15..8478bd4e 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,6 +1,6 @@
-The Coq proof assistant V7 and V8 includes software developed by the
-Coq development team inside the LogiCal project, at INRIA, CNRS and
-University Paris Sud.
+The Coq proof assistant V7 and V8 includes software developed by the
+Coq development team inside the TypiCal (formerly LogiCal) project, at
+INRIA, CNRS and University Paris Sud.
Copyright 1999-2004 The Coq development team,
INRIA-CNRS, University Paris Sud, All rights reserved.
@@ -19,17 +19,9 @@ parsing/search.ml)
Pierre Courtieu, Lemme (contrib/funind)
Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
+ Lionel Mamane, Radbout University, Nijmegen (additions to contrib/interface)
+ Cezary Kalyczyc, Radbout University, Nijmegen (additions to contrib/xml)
The file CREDITS contains a list of past contributors
The credits section in Reference Manual introduction details
contributions.
-
-The Coq development Team (march 2004)
- Bruno Barras (INRIA)
- Pierre Corbineau (Université Paris Sud)
- Jean-Christophe Filliâtre (CNRS)
- Hugo Herbelin (INRIA)
- Pierre Letouzey (Université Paris Sud)
- Claude Marché (Université Paris Sud-INRIA)
- Christine Paulin (Université Paris Sud)
- Clément Renard (INRIA)
diff --git a/CREDITS b/CREDITS
index b3d563ca..90dbd0b2 100644
--- a/CREDITS
+++ b/CREDITS
@@ -50,8 +50,6 @@ contrib/interface
at Nijmegen, 2007-2008)
contrib/omega
developed by Pierre Crégut (France Telecom R&D, 1996)
-contrib/recdef
- developed by Yves Bertot (INRIA-Marelle, 2005-2006)
contrib/ring
developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
Loiseleur (LRI, 1997-1999)
@@ -80,16 +78,21 @@ theories/ZArith
started by Pierre Crégut (France Telecom R&D, 1996)
theories/IntMap
developed by Jean Goubault-Larrecq (Dyade, 1998)
+theories/Numbers/Cyclic
+ developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry
+ (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and
+ Pierre Letouzey (PPS-Paris 7, 2008)
theories/Strings
developed by Laurent Théry (INRIA-Lemme, 2003)
ide/utils
some files come from Maxence Guesdon's Cameleon tool
-Many discussions within the Démons team at LRI and the LogiCal project
-influenced significantly the design of Coq especially with
+Many discussions within the Démons team at LRI, and the
+LogiCal/TypiCal projects influenced significantly the design of
+components of Coq, especially with
- J. Courant, P. Courtieu, J. Duprat, J. Goubault,
- A. Miquel, C. Marché, B. Monate, B. Werner.
+ F. Blanqui, J. Courant, P. Courtieu, J. Duprat, S. Glondu, J. Goubault,
+ A. Mahboubi, C. Marché, A. Miquel, B. Monate, P.-Y. Strub, B. Werner.
Intensive users suggested improvements of the system :
@@ -135,9 +138,11 @@ of the Coq Proof assistant during the indicated time :
LRI, 1997-now)
Clément Renard (INRIA, 2001-2004)
Claudio Sacerdoti Coen (INRIA, 2004-2005)
+ Amokrane Saïbi (INRIA, 1993-1998)
+ Vincent Siles (INRIA, 2007)
+ Élie Soubiran (INRIA, 2007-now)
Matthieu Sozeau (INRIA, 2005-now)
Arnaud Spiwack (INRIA, 2006-now)
- Amokrane Saïbi (INRIA, 1993-1998)
Benjamin Werner (INRIA, 1989-1994)
***************************************************************************
diff --git a/Makefile b/Makefile
index 70e9fb1f..6854de92 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 11826 2009-01-22 06:43:35Z notin $
+# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $
# Makefile for Coq
@@ -24,14 +24,17 @@
# by Emacs' next-error.
###########################################################################
+export SHELL:=/bin/bash
+
export FIND_VCS_CLAUSE:='(' \
- -name '{arch}' -or \
- -name '.svn' -or \
- -name '_darcs' -or \
- -name '.git' -or \
- -name 'debian' -or \
+ -name '{arch}' -o \
+ -name '.svn' -o \
+ -name '_darcs' -o \
+ -name '.git' -o \
+ -name '.bzr' -o \
+ -name 'debian' -o \
-name "$${GIT_DIR}" \
-')' -prune -type f -or
+')' -prune -type f -o
export PRUNE_CHECKER := -wholename ./checker/\* -prune -or
FIND_PRINTF_P:=-print | sed 's|^\./||'
@@ -45,7 +48,7 @@ export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \
- while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \
+ while read f; do if [ ! -e "$${f}4" ]; then echo "$$f"; fi; done) \
$(GENMLFILES)
export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
$(GENMLIFILES)
@@ -152,15 +155,15 @@ clean: objclean cruftclean depclean docclean devdocclean
objclean: archclean indepclean
cruftclean: ml4clean
- find . -name '*~' -or -name '*.annot' | xargs rm -f
+ find . -name '*~' -o -name '*.annot' | xargs rm -f
rm -f gmon.out core
indepclean:
rm -f $(GENFILES)
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 test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
+ find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
+ find contrib test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
rm -f */*.pp[iox] contrib/*/*.pp[iox]
rm -rf $(SOURCEDOCDIR)
rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -184,12 +187,13 @@ docclean:
rm -f doc/common/version.tex
rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
rm -f doc/coq.tex
+ rm -f doc/refman/styles.hva doc/refman/cover.html
archclean: clean-ide cleantheories
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
+ find . -name '*.cmx' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
rm -f $(TOOLS) $(CSDPCERT)
clean-ide:
@@ -214,7 +218,7 @@ distclean: clean cleanconfig
cleantheories:
rm -f states/*.coq
- find theories -name '*.vo' -or -name '*.glob' | xargs rm -f
+ find theories -name '*.vo' -o -name '*.glob' | xargs rm -f
devdocclean:
find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \;
diff --git a/Makefile.build b/Makefile.build
index 19f13f15..703c5884 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile.build 11935 2009-02-17 16:14:07Z notin $
+# $Id: Makefile.build 12169 2009-06-06 21:43:23Z herbelin $
# Makefile for Coq
@@ -717,7 +717,7 @@ ifeq ($(BEST),opt)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
- -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
+ -$(MKDIR) $(FULLCOQLIB)/contrib/micromega
$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
-$(INSTALLLIB) revision $(FULLCOQLIB)
@@ -960,7 +960,7 @@ else
endif
%.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
$(SHOW)'CAMLP4DEPS $<'
- $(HIDE)( /bin/echo -n '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
+ $(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
|| ( RV=$$?; rm -f "$@"; exit $${RV} )
%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d
diff --git a/Makefile.common b/Makefile.common
index 15faace0..d6f43cf5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -210,12 +210,11 @@ TACTICS:=\
tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
tactics/nbtermdn.cmo tactics/tacticals.cmo \
tactics/hipattern.cmo tactics/tactics.cmo \
- tactics/evar_tactics.cmo \
tactics/hiddentac.cmo tactics/elim.cmo \
tactics/dhyp.cmo tactics/auto.cmo \
toplevel/ind_tables.cmo tactics/equality.cmo \
tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \
- tactics/tacinterp.cmo tactics/autorewrite.cmo \
+ tactics/tacinterp.cmo tactics/autorewrite.cmo tactics/evar_tactics.cmo \
tactics/decl_interp.cmo tactics/decl_proof_instr.cmo
TOPLEVEL:=\
diff --git a/Makefile.doc b/Makefile.doc
index aff812db..795e0e5c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -125,7 +125,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
$(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;\
@@ -184,40 +184,32 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
### Standard library (browsable html format)
ifeq ($(QUICK),1)
-doc/stdlib/index-body.html:
- - rm -rf doc/stdlib/html
- $(MKDIR) doc/stdlib/html
- $(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \
- -R theories Coq $(THEORIESVO:.vo=.v)
- mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+doc/stdlib/html/genindex.html:
else
-doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO)
+doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
+endif
- rm -rf doc/stdlib/html
$(MKDIR) doc/stdlib/html
- $(COQDOC) -q -d doc/stdlib/html --multi-index --html -g \
+ $(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
-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>/,/<\/table>/p' doc/stdlib/index-body.html >> $@
- cat doc/stdlib/index-trailer.html >> $@
+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)
ifeq ($(QUICK),1)
doc/stdlib/Library.coqdoc.tex:
- $(COQDOC) -q -boot --gallina --body-only --latex --stdout \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
else
doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
+endif
$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
-endif
doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
(cd doc/stdlib;\
diff --git a/Makefile.stage1 b/Makefile.stage1
index a60d388f..c39a6372 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -6,6 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
+export SHELL:=/bin/bash
include Makefile.build
# All includes must be declared secondary, otherwise make will delete
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 9e886837..f4ffb302 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -108,7 +108,7 @@ type compiled_library =
open Validate
let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_eng|]
+let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
(* This function should append a certificate to the .vo file.
The digest must be part of the certicate to rule out attackers
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 14595fa5..0dc4a6a8 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 11858 2009-01-26 13:27:23Z notin $ i*)
+(*i $Id: coq_config.mli 12104 2009-04-24 18:10:10Z notin $ i*)
val local : bool (* local use (no installation) *)
@@ -45,4 +45,8 @@ val browser : string
(** default web browser to use, may be overriden by environment
variable COQREMOTEBROWSER *)
+val wwwcoq : string
+val wwwrefman : string
+val wwwstdlib : string
+
val has_natdynlink : bool
diff --git a/configure b/configure
index c8508f52..1ba4eaba 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
##################################
#
@@ -6,8 +6,8 @@
#
##################################
-VERSION=8.2
-VOMAGIC=08200
+VERSION=8.2pl1
+VOMAGIC=08200
STATEMAGIC=58200
DATE=`LANG=C date +"%B %Y"`
@@ -133,6 +133,7 @@ reals=all
arch_spec=no
coqide_spec=no
browser_spec=no
+wwwcoq_spec=no
with_geoproof=false
with_doc=all
with_doc_spec=no
@@ -216,6 +217,9 @@ while : ; do
-browser|--browser) browser_spec=yes
BROWSER=$2
shift;;
+ -coqwebsite|--coqwebsite) wwwcoq_spec=yes
+ WWWCOQ=$2
+ shift;;
-with-doc|--with-doc) with_doc_spec=yes
case "$2" in
yes|all) with_doc=all;;
@@ -285,7 +289,7 @@ case $arch_spec in
ARCH=`/usr/bin/uname -s`
else
echo "I can not automatically find the name of your architecture"
- echo -n\
+ printf "%s"\
"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
read ARCH
fi
@@ -358,6 +362,10 @@ if [ "$browser_spec" = "no" ]; then
esac
fi
+if [ "$wwwcoq_spec" = "no" ]; then
+ WWWCOQ="http://www.lix.polytechnique.fr/coq/"
+fi
+
#########################################
# Objective Caml programs
@@ -853,6 +861,7 @@ echo " Documentation : None"
fi
echo " CoqIde : $COQIDE"
echo " Web browser : $BROWSER"
+echo " Coq web site : $WWWCOQ"
echo ""
echo " Paths for true installation:"
@@ -944,6 +953,9 @@ let state_magic_number = $STATEMAGIC
let exec_extension = "$EXE"
let with_geoproof = ref $with_geoproof
let browser = "$ESCBROWSER"
+let wwwcoq = "$WWWCOQ"
+let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
+let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
END_OF_COQ_CONFIG
@@ -1068,4 +1080,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 11934 2009-02-17 15:58:54Z notin $
+# $Id: configure 12219 2009-07-01 09:58:00Z notin $
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index e59de34a..e0f43193 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
| Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
| Intro identifier -> "Intro"
| Cut (bool, _, identifier, types) -> "Cut"
- | FixRule (identifier, int, l) -> "FixRule"
- | Cofix (identifier, l) -> "Cofix"
+ | FixRule (identifier, int, l, _) -> "FixRule"
+ | Cofix (identifier, l, _) -> "Cofix"
| Convert_concl (types, cast_kind) -> "Convert_concl"
| Convert_hyp named_declaration -> "Convert_hyp"
| Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
| Refine c -> depends_of_constr c acc
| Intro id -> acc
| Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
- | FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
- | Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+ | FixRule (_, _, l, _) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+ | Cofix (_, l, _) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
| Convert_concl (t, _) -> depends_of_constr t acc
| Convert_hyp (_, None, t) -> depends_of_constr t acc
| Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ba00fce5..c0b64379 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
open Global
open Pp
@@ -99,7 +99,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
in
let c = solve_tccs_in_type env id isevars evm c typ in
- List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
+ List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
else
errorlabstrm "Command.Assumption"
(str "Cannot declare an assumption while in proof editing mode.")
@@ -127,7 +127,6 @@ let check_fresh (loc,id) =
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
- check_required_library ["Coq";"Program";"Tactics"];
let env = Global.env () in
let isevars = ref (create_evar_defs Evd.empty) in
try
@@ -143,7 +142,7 @@ let subtac (loc, command) =
start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
(fun _ _ -> ())
| DefineBody (bl, _, c, tycon) ->
- ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon))
+ ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
| VernacFixpoint (l, b) ->
List.iter (fun ((lid, _, _, _, _), _) ->
check_fresh lid;
@@ -237,9 +236,6 @@ let subtac (loc, command) =
debug 2 (Himsg.explain_pretype_error env exn);
raise e
- | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
- raise e)
+ | e'' -> raise e)
- | e ->
- msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
- raise e
+ | e -> raise e
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 1d213db9..bd06407f 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
open Cases
open Util
@@ -301,8 +301,8 @@ module Cases_F(Coercion : Coercion.S) : S = struct
let inh_coerce_to_ind isevars env ty tyi =
let expected_typ = inductive_template isevars env None tyi in
- (* devrait être indifférent d'exiger leq ou pas puisque pour
- un inductif cela doit être égal *)
+ (* devrait être indifférent d'exiger leq ou pas puisque pour
+ un inductif cela doit être égal *)
let _ = e_cumul env isevars expected_typ ty in ()
let unify_tomatch_with_patterns isevars env loc typ pats =
@@ -696,9 +696,9 @@ let insert_aliases_eqn sign eqnnames alias_rest eqn =
let insert_aliases env sigma alias eqns =
- (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
- (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
- (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
+ (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
+ (* défaut présent mais inutile, ce qui est le cas général, l'alias *)
+ (* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
(* names2 takes the meet of all needed aliases *)
@@ -843,7 +843,7 @@ let infer_predicate loc env isevars typs cstrs indf =
(* Non dependent case -> turn it into a (dummy) dependent one *)
let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
- (true,pred) (* true = dependent -- par défaut *)
+ (true,pred) (* true = dependent -- par défaut *)
else
(*
let s = get_sort_of env (evars_of isevars) typs.(0) in
@@ -1294,7 +1294,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
List.fold_left mkSpecialLetInJudge j sign
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
-substituer après par les initiaux *)
+substituer après par les initiaux *)
(**************************************************************************)
(* Preparation of the pattern-matching problem *)
@@ -1319,99 +1319,6 @@ let matx_of_eqns env eqns =
(************************************************************************)
(* preparing the elimination predicate if any *)
-let build_expected_arity env isevars isdep tomatchl =
- let cook n = function
- | _,IsInd (_,IndType(indf,_)) ->
- let indf' = lift_inductive_family n indf in
- Some (build_dependent_inductive env indf', fst (get_arity env indf'))
- | _,NotInd _ -> None
- in
- let rec buildrec n env = function
- | [] -> new_Type ()
- | tm::ltm ->
- match cook n tm with
- | None -> buildrec n env ltm
- | Some (ty1,aritysign) ->
- let rec follow n env = function
- | d::sign ->
- mkProd_or_LetIn_name env
- (follow (n+1) (push_rel d env) sign) d
- | [] ->
- if isdep then
- mkProd (Anonymous, ty1,
- buildrec (n+1)
- (push_rel_assum (Anonymous, ty1) env)
- ltm)
- else buildrec n env ltm
- in follow n env (List.rev aritysign)
- in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
- let cook = function
- | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
- | _,NotInd _ -> None in
- let rec decomp_lam_force n l p =
- if n=0 then (l,p) else
- match kind_of_term p with
- | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
- | _ -> (* eta-expansion *)
- let na = Name (id_of_string "x") in
- decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
- let rec buildrec allnames p = function
- | [] -> (List.rev allnames,p)
- | tm::ltm ->
- match cook tm with
- | None ->
- let p =
- (* adjust to a sign containing the NotInd's *)
- if isdep then lift 1 p else p in
- let names = if isdep then [Anonymous] else [] in
- buildrec (names::allnames) p ltm
- | Some n ->
- let n = if isdep then n+1 else n in
- let names,p = decomp_lam_force n [] p in
- buildrec (names::allnames) p ltm
- in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
- (* avoid is not exhaustive ! *)
- let rec decomp_lam_force n avoid l p =
- if n = 0 then (List.rev l,p,avoid) else
- match p with
- | RLambda (_,(Name id as na),k,_,c) ->
- decomp_lam_force (n-1) (id::avoid) (na::l) c
- | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
- | _ ->
- let x = next_ident_away (id_of_string "x") avoid in
- decomp_lam_force (n-1) (x::avoid) (Name x :: l)
- (* eta-expansion *)
- (let a = RVar (dummy_loc,x) in
- match p with
- | RApp (loc,p,l) -> RApp (loc,p,l@[a])
- | _ -> (RApp (dummy_loc,p,[a]))) in
- let rec decomp_block avoid p = function
- | ([], _) -> x := Some p
- | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') ->
- let (ind,params) = dest_ind_family indf in
- let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p
- in
- let na,p,avoid' =
- if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
- in
- y :=
- (List.hd na,
- if List.for_all ((=) Anonymous) nal then
- None
- else
- Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
- decomp_block avoid' p (l,l')
- | (_::l),(y::l') ->
- y := (Anonymous,None);
- decomp_block avoid p (l,l')
- | _ -> anomaly "set_arity_signature"
- in
- decomp_block [] pred (tomatchl,arsign)
-
let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
let cook (n, l, env, signs) = function
| c,IsInd (_,IndType(indf,realargs)) ->
@@ -1569,9 +1476,6 @@ let eq_id avoid id =
let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y =
- mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
@@ -1828,24 +1732,6 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
* A type constraint but no annotation case: it is assumed non dependent.
*)
-
-let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
- (* We extract the signature of the arity *)
- let arsign = extract_arity_signature env tomatchs sign in
- let env = List.fold_right push_rels arsign env in
- let allnames = List.rev (List.map (List.map pi1) arsign) in
- match rtntyp with
- | Some rtntyp ->
- let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
- let predccl = (j_nf_isevar !isevars predcclj).uj_val in
- Some (build_initial_predicate true allnames predccl)
- | None ->
- match valcon_of_tycon tycon with
- | Some ty ->
- let names,pred =
- oldprepare_predicate_from_tycon loc false env isevars tomatchs sign ty
- in Some (build_initial_predicate true names pred)
- | None -> None
let lift_ctx n ctx =
let ctx', _ =
@@ -1862,7 +1748,7 @@ let abstract_tomatch env tomatchs =
Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
| _ ->
let name = next_ident_away_from (id_of_string "filtered_var") names in
- (mkRel 1, lift_tomatch_type 1 t) :: lift_ctx 1 prev,
+ (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
(Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
name :: names)
([], [], []) tomatchs
@@ -1912,7 +1798,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
let previd, id =
let name =
match kind_of_term arg with
- Rel n -> pi1 (lookup_rel n (rel_context env))
+ Rel n -> pi1 (Environ.lookup_rel n env)
| _ -> name
in
make_prime avoid name
@@ -2025,6 +1911,25 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
ignore(Typing.sort_of env' evm pred); pred
with _ -> lift nar c
+
+let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
+ (* We extract the signature of the arity *)
+ let arsign = extract_arity_signature env tomatchs sign in
+ let newenv = List.fold_right push_rels arsign env in
+ let allnames = List.rev (List.map (List.map pi1) arsign) in
+ match rtntyp with
+ | Some rtntyp ->
+ let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
+ let predccl = (j_nf_isevar !isevars predcclj).uj_val in
+ Some (build_initial_predicate true allnames predccl)
+ | None ->
+ match valcon_of_tycon tycon with
+ | Some ty ->
+ let pred =
+ prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs arsign ty
+ in Some (build_initial_predicate true allnames pred)
+ | None -> None
+
let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
let typing_fun tycon env = typing_fun tycon env isevars in
@@ -2103,26 +2008,25 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
(* with the type of arguments to match *)
let tmsign = List.map snd tomatchl in
let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
-
- (* We push the initial terms to match and push their alias to rhs' envs *)
- (* names of aliases will be recovered from patterns (hence Anonymous here) *)
- let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
-
- let pb =
- { env = env;
- isevars = isevars;
- pred = pred;
- tomatch = initial_pushed;
- history = start_history (List.length initial_pushed);
- mat = matx;
- caseloc = loc;
- casestyle= style;
- typing_function = typing_fun } in
-
- let j = compile pb in
- (* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
- inh_conv_coerce_to_tycon loc env isevars j tycon
+ (* We push the initial terms to match and push their alias to rhs' envs *)
+ (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+ let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+ let pb =
+ { env = env;
+ isevars = isevars;
+ pred = pred;
+ tomatch = initial_pushed;
+ history = start_history (List.length initial_pushed);
+ mat = matx;
+ caseloc = loc;
+ casestyle= style;
+ typing_function = typing_fun } in
+
+ let j = compile pb in
+ (* We check for unused patterns *)
+ List.iter (check_unused_pattern env) matx;
+ inh_conv_coerce_to_tycon loc env isevars j tycon
+
end
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0d44a0c0..9b692d85 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
open Pretyping
open Evd
@@ -182,7 +182,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
in
isevars := undefined_evars !isevars;
Evarutil.check_evars env Evd.empty !isevars termtype;
- let hook gr =
+ let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global cst in
Impargs.declare_manual_implicits false gr ~enriching:false imps;
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 4876b065..c8c7ff72 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -390,7 +390,7 @@ let interp_recursive fixkind l boxed =
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
- States.with_heavy_rollback (fun () ->
+ States.with_state_protection (fun () ->
List.iter (Command.declare_interning_data impls) notations;
list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
() in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index d2e831ef..3dcd43d2 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -17,8 +17,6 @@ open Evd
open Declare
open Proof_type
-type definition_hook = global_reference -> unit
-
let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Util.errorlabstrm "Program" cmd
let error s = pperror (str s)
@@ -56,14 +54,14 @@ type program_info = {
prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
prg_notations : notations ;
prg_kind : definition_kind;
- prg_hook : definition_hook;
+ prg_hook : Tacexpr.declaration_hook;
}
let assumption_message id =
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
@@ -203,7 +201,7 @@ let declare_definition prg =
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
Impargs.declare_manual_implicits false gr prg.prg_implicits;
print_message (Subtac_utils.definition_message prg.prg_name);
- prg.prg_hook gr;
+ prg.prg_hook local gr;
gr
open Pp
@@ -234,6 +232,7 @@ let reduce_fix =
let declare_mutual_definition l =
let len = List.length l in
+ let first = List.hd l in
let fixdefs, fixtypes, fiximps =
list_split3
(List.map (fun x ->
@@ -241,11 +240,11 @@ let declare_mutual_definition l =
snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
- let fixkind = Option.get (List.hd l).prg_fixkind in
+ let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
- let boxed = true (* TODO *) in
- let fixnames = (List.hd l).prg_deps in
+ let (local,boxed,kind) = first.prg_kind in
+ let fixnames = first.prg_deps in
let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
@@ -260,9 +259,11 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
- List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+ List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
- (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+ let gr = List.hd kns in
+ let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+ first.prg_hook local gr; kn
let declare_obligation obl body =
match obl.obl_status with
@@ -525,7 +526,7 @@ let show_term n =
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ my_print_constr (Global.env ()) prg.prg_body)
-let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let prg = init_prog_info n b t [] None [] obls implicits kind hook in
let obls,_ = prg.prg_obligations in
@@ -543,11 +544,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
- let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun x -> ()) in
+ let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
ProgMap.add n prg acc)
!from_prg l
in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 60c0a413..766af2fa 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -21,13 +21,11 @@ val default_tactic : unit -> Proof_type.tactic
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
-type definition_hook = global_reference -> unit
-
val add_definition : Names.identifier -> Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
- ?hook:definition_hook -> obligation_info -> progress
+ ?hook:Tacexpr.declaration_hook -> obligation_info -> progress
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -36,6 +34,7 @@ val add_mutual_definitions :
(Topconstr.explicitation * (bool * bool)) list * obligation_info) list ->
?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
+ ?hook:Tacexpr.declaration_hook ->
notations ->
Command.fixpoint_kind -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 07a75720..3ae7c95d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Global
open Pp
@@ -84,13 +84,6 @@ let find_with_index x l =
| [] -> raise Not_found
in aux 0 l
-let list_split_at index l =
- let rec aux i acc = function
- hd :: tl when i = index -> (List.rev acc), tl
- | hd :: tl -> aux (succ i) (hd :: acc) tl
- | [] -> failwith "list_split_at: Invalid argument"
- in aux 0 [] l
-
open Vernacexpr
let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
@@ -136,9 +129,9 @@ let subtac_process env isevars id bl c tycon =
open Subtac_obligations
-let subtac_proof kind env isevars id bl c tycon =
+let subtac_proof kind hook env isevars id bl c tycon =
let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
let evm' = Subtac_utils.evars_of_term evm evm' coqt in
let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
- add_definition id def ty ~implicits:imps ~kind:kind evars
+ add_definition id def ty ~implicits:imps ~kind ~hook evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 1d8eb250..ba0b7cd2 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -19,5 +19,6 @@ val interp :
val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
-val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list ->
+val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook ->
+ env -> evar_defs ref -> identifier -> local_binder list ->
constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index cdbc4023..2ee2018e 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -64,15 +64,17 @@ let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
-let jmeq_ind =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq")
-let jmeq_rec =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_rec")
-let jmeq_refl =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_refl")
+let jmeq_ind () =
+ check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq"
+
+let jmeq_rec () =
+ check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_rec"
+
+let jmeq_refl () =
+ check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_refl"
let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
@@ -277,8 +279,8 @@ let mkSubset name typ prop =
let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (jmeq_ind (), [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (jmeq_refl (), [| typ; x |])
let unsafe_fold_right f = function
hd :: tl -> List.fold_right f tl hd
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 964f668f..9c014286 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -45,9 +45,9 @@ val and_typ : constr lazy_t
val eqdep_ind : constr lazy_t
val eqdep_rec : constr lazy_t
-val jmeq_ind : constr lazy_t
-val jmeq_rec : constr lazy_t
-val jmeq_refl : constr lazy_t
+val jmeq_ind : unit -> constr
+val jmeq_rec : unit -> constr
+val jmeq_refl : unit -> constr
val boolind : constr lazy_t
val sumboolind : constr lazy_t
@@ -103,7 +103,7 @@ val mk_ex_pi1 : constr -> constr -> constr -> constr
val mk_ex_pi1 : constr -> constr -> constr -> constr
val mk_eq : types -> constr -> constr -> types
val mk_eq_refl : types -> constr -> constr
-val mk_JMeq : types -> constr-> types -> constr -> types
+val mk_JMeq : types -> constr -> types -> constr -> types
val mk_JMeq_refl : types -> constr -> constr
val mk_conj : types list -> types
val mk_not : types -> types
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index a501fb6a..7503d632 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
let string_of_prim_rule x = match x with
| Proof_type.Intro _-> "Intro"
| Proof_type.Cut _ -> "Cut"
- | Proof_type.FixRule (_,_,_) -> "FixRule"
- | Proof_type.Cofix (_,_)-> "Cofix"
+ | Proof_type.FixRule _ -> "FixRule"
+ | Proof_type.Cofix _ -> "Cofix"
| Proof_type.Refine _ -> "Refine"
| Proof_type.Convert_concl _ -> "Convert_concl"
| Proof_type.Convert_hyp _->"Convert_hyp"
diff --git a/dev/base_include b/dev/base_include
index d4366843..711dcb2a 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -14,6 +14,9 @@
#directory "tactics";;
#directory "translate";;
+#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
+#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
+
#use "top_printers.ml";;
#use "vm_printers.ml";;
@@ -112,6 +115,9 @@ open Proof_type
open Redexpr
open Refiner
open Tacmach
+open Decl_proof_instr
+open Tactic_debug
+open Decl_mode
open Auto
open Autorewrite
diff --git a/doc/stdlib/index-trailer.html b/doc/common/styles/html/simple/footer.html
index 308b1d01..308b1d01 100644
--- a/doc/stdlib/index-trailer.html
+++ b/doc/common/styles/html/simple/footer.html
diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html
new file mode 100644
index 00000000..14d2f988
--- /dev/null
+++ b/doc/common/styles/html/simple/header.html
@@ -0,0 +1,13 @@
+<!DOCTYPE html
+ PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+
+<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
+<link rel="stylesheet" href="coqdoc.css" type="text/css"/>
+<title>The Coq Standard Library</title>
+</head>
+
+<body>
+
diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css
new file mode 100644
index 00000000..0b1e640b
--- /dev/null
+++ b/doc/common/styles/html/simple/style.css
@@ -0,0 +1,13 @@
+#footer {
+ border-top: solid black 1pt;
+ text-align: center;
+ text-indent: 0pt;
+}
+
+.menu { }
+.menu li {
+ display: inline;
+ margin: 0pt;
+ padding: .5ex 1em;
+ list-style: none
+} \ No newline at end of file
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0ab4e47b..484002c3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -1,17 +1,5 @@
-<!DOCTYPE html
- PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
- "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/>
-<link rel="stylesheet" href="css/context.css" type="text/css"/>
-<title>The Coq Standard Library</title>
-</head>
-
-<body>
-
-<H1>The Coq Standard Library</H1>
+<h1>The Coq Standard Library</h1>
<p>Here is a short description of the Coq standard library, which is
distributed with the system.
@@ -323,8 +311,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
<dd>
theories/Setoids/Setoid.v
- theories/Setoids/Setoid_tac.v
- theories/Setoids/Setoid_Prop.v
</dd>
<dt> <b>Lists</b>:
diff --git a/ide/coq.ml b/ide/coq.ml
index e2649c82..a44428c7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 11826 2009-01-22 06:43:35Z notin $ *)
+(* $Id: coq.ml 11948 2009-02-27 16:01:53Z glondu $ *)
open Vernac
open Vernacexpr
@@ -424,6 +424,8 @@ let interp_with_options verbosely options s =
prerr_endline s;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
+ (* Temporary hack to make coqide.byte work (WTF???) *)
+ Pervasives.prerr_endline "";
match pe with
| None -> assert false
| Some((loc,vernac) as last) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ea2dfe4d..cc147d5e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *)
+(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
open Preferences
open Vernacexpr
@@ -3237,7 +3237,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~callback:
(fun () ->
let av = Option.get ((get_current_view ()).analyzed_view) in
- browse av#insert_message (!current.doc_url ^ "main.html")) in
+ browse av#insert_message (!current.doc_url)) in
let _ = help_factory#add_item "Browse Coq _Library"
~callback:
(fun () ->
@@ -3518,8 +3518,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let about_full_string =
"\nCoq is developed by the Coq Development Team\
\n(INRIA - CNRS - University Paris 11 and partners)\
- \nWeb site: http://coq.inria.fr\
- \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
+ \nWeb site: " ^ Coq_config.wwwcoq ^
+ "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
\n\
\nCredits for CoqIDE, the Integrated Development Environment for Coq:\
\n\
diff --git a/ide/preferences.ml b/ide/preferences.ml
index dba56a77..ffb346d9 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: preferences.ml 11276 2008-07-28 00:28:34Z glondu $ *)
+(* $Id: preferences.ml 12104 2009-04-24 18:10:10Z notin $ *)
open Configwin
open Printf
@@ -135,8 +135,8 @@ let (current:pref ref) =
(* text_font = Pango.Font.from_string "sans 12";*)
text_font = Pango.Font.from_string "Monospace 10";
- doc_url = "http://coq.inria.fr/doc/";
- library_url = "http://coq.inria.fr/library/";
+ doc_url = Coq_config.wwwrefman;
+ library_url = Coq_config.wwwstdlib;
show_toolbar = true;
contextual_menus_on_goal = true;
diff --git a/install.sh b/install.sh
index 277222f5..c2f8215b 100755
--- a/install.sh
+++ b/install.sh
@@ -1,4 +1,4 @@
-#! /bin/sh
+#! /bin/bash
dest="$1"
shift
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 86e02623..cd4efe27 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: environ.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Util
open Names
@@ -554,7 +554,7 @@ fun env field value ->
type context_object =
| Variable of identifier (* A section variable or a Let definition *)
| Axiom of constant (* An axiom or a constant. *)
-
+ | Opaque of constant (* An opaque constant. *)
(* Defines a set of [assumption] *)
module OrderedContextObject =
@@ -566,15 +566,19 @@ struct
| Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
(* spiwack: it would probably be cleaner
to provide a [kn_ord] function *)
+ | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
| Variable _ , Axiom _ -> -1
| Axiom _ , Variable _ -> 1
+ | Opaque _ , _ -> -1
+ | _, Opaque _ -> 1
end
module ContextObjectSet = Set.Make (OrderedContextObject)
module ContextObjectMap = Map.Make (OrderedContextObject)
-let assumptions (* t env *) =
+let assumptions ?(add_opaque=false) st (* t env *) =
+ let (idts,knst) = st in
(* Infix definition for chaining function that accumulate
on a and a ContextObjectSet, ContextObjectMap. *)
let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
@@ -650,16 +654,26 @@ let assumptions (* t env *) =
and add_kn kn env s acc =
let cb = lookup_constant kn env in
- match cb.Declarations.const_body with
- | None ->
- let ctype =
- match cb.Declarations.const_type with
- | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
- | NonPolymorphicType t -> t
- in
- (s,ContextObjectMap.add (Axiom kn) ctype acc)
- | Some body -> aux (Declarations.force body) env s acc
-
+ let do_type cst =
+ let ctype =
+ match cb.Declarations.const_type with
+ | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+ | NonPolymorphicType t -> t
+ in
+ (s,ContextObjectMap.add cst ctype acc)
+ in
+ let (s,acc) =
+ if cb.Declarations.const_body <> None
+ && (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
+ && add_opaque
+ then
+ do_type (Opaque kn)
+ else (s,acc)
+ in
+ match cb.Declarations.const_body with
+ | None -> do_type (Axiom kn)
+ | Some body -> aux (Declarations.force body) env s acc
+
and aux_memoize_kn kn env =
try_and_go (Axiom kn) (add_kn kn env)
in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 97e19782..b68123f6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: environ.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Names
@@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env
type context_object =
| Variable of identifier (* A section variable or a Let definition *)
| Axiom of constant (* An axiom or a constant. *)
+ | Opaque of constant (* An opaque constant. *)
(* AssumptionSet.t is a set of [assumption] *)
module OrderedContextObject : Set.OrderedType with type t = context_object
module ContextObjectMap : Map.S with type key = context_object
-(* collects all the assumptions on which a term relies (together with
- their type *)
-val assumptions : constr -> env -> Term.types ContextObjectMap.t
+(* collects all the assumptions (optionally including opaque definitions)
+ on which a term relies (together with their type) *)
+val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ab4b8e47..9a76922b 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *)
+(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
open Pp
open Util
@@ -250,11 +250,11 @@ let join (subst1 : substitution) (subst2 : substitution) =
try
let res =
match resolve with
- Some res -> res
- | None ->
+ |None -> begin
match resolve' with
None -> raise BothSubstitutionsAreIdentitySubstitutions
- | Some res -> raise (ChangeDomain res)
+ | Some res -> raise (ChangeDomain res) end
+ | Some res -> res
in
Some
(List.map
@@ -356,23 +356,23 @@ let update_subst subst1 subst2 =
| MPI mp -> mp
in
match mp with
- | MPbound mbid -> ((MBI mbid),newmp)::l
- | MPself msid -> ((MSI msid),newmp)::l
- | _ -> ((MPI mp),newmp)::l
+ | MPbound mbid -> ((MBI mbid),newmp,resolve)::l
+ | MPself msid -> ((MSI msid),newmp,resolve)::l
+ | _ -> ((MPI mp),newmp,resolve)::l
in
let subst_mbi = Umap.fold subst_inv subst2 [] in
let alias_subst key (mp,resolve) sub=
let newsetkey =
match key with
| MPI mp1 ->
- let compute_set_newkey l (k,mp') =
+ let compute_set_newkey l (k,mp',resolve) =
let mp_from_key = match k with
| MBI msid -> MPbound msid
| MSI msid -> MPself msid
| MPI mp -> mp
in
let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
- if new_mp1 == mp1 then l else (MPI new_mp1)::l
+ if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
in
begin
match List.fold_left compute_set_newkey [] subst_mbi with
@@ -384,7 +384,7 @@ let update_subst subst1 subst2 =
match newsetkey with
| None -> sub
| Some l ->
- List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+ List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
sub l
in
Umap.fold alias_subst subst1 empty_subst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 25a11c69..949a7402 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
+(*i $Id: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
(*i*)
open Util
@@ -272,9 +272,9 @@ let rec eval_struct env = function
(subst_key (map_msid msid mp) sub_alias)
(map_msid msid mp)
| _ -> sub_alias in
- let sub_alias1 = update_subst sub_alias
- (map_mbid farg_id mp (None)) in
- let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
+ let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
+ let sub_alias1 = update_subst sub_alias
+ (map_mbid farg_id mp (Some resolve)) in
eval_struct env (subst_struct_expr
(join sub_alias1
(map_mbid farg_id mp (Some resolve))) fbody_b)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fbb05a2d..7a2db86b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *)
+(* $Id: safe_typing.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Util
open Names
@@ -113,7 +113,7 @@ let add_constraints cst senv =
(* terms which are closed under the environnement env, i.e
terms which only depends on constant who are themselves closed *)
let closed env term =
- ContextObjectMap.is_empty (assumptions env term)
+ ContextObjectMap.is_empty (assumptions full_transparent_state env term)
(* the set of safe terms in an environement any recursive set of
terms who are known not to prove inconsistent statement. It should
diff --git a/lib/util.ml b/lib/util.ml
index a8a99c0b..dce36419 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *)
open Pp
@@ -257,7 +257,7 @@ let classify_unicode unicode =
(* utf-8 arrows and brackets U27E0-U27FF *)
| x when 0x27E0 <= x & x <= 0x27FF -> UnicodeSymbol
(* utf-8 brackets, braces and parentheses *)
- | x when 0x2980 <= x & x <= 0x299F -> UnicodeSymbol
+ | x when 0x2980 <= x & x <= 0x29FF -> UnicodeSymbol
(* utf-8 miscellaneous including double-plus U29F0-U29FF *)
| x when 0x29F0 <= x & x <= 0x29FF -> UnicodeSymbol
| _ -> raise UnsupportedUtf8
diff --git a/library/declare.ml b/library/declare.ml
index 4bdc11c3..c349bef1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
(** This module is about the low-level declaration of logical objects *)
@@ -43,7 +43,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
- | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+ | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
type variable_declaration = dir_path * section_variable_entry * logical_kind
@@ -58,7 +58,7 @@ let cache_variable ((sp,_),o) =
| SectionLocalAssum (ty, impl, keep) ->
let cst = Global.push_named_assum (id,ty) in
let impl = if impl then Lib.Implicit else Lib.Explicit in
- let keep = if keep then Some ty else None in
+ let keep = if keep <> [] then Some (ty, keep) else None in
impl, true, cst, keep
| SectionLocalDef (c,t,opaq) ->
let cst = Global.push_named_def (id,c,t) in
diff --git a/library/declare.mli b/library/declare.mli
index 78d3f027..2f1cd06e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declare.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Names
@@ -34,7 +34,7 @@ open Nametab
type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
- | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
+ | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
type variable_declaration = dir_path * section_variable_entry * logical_kind
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3026143b..93021384 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
+(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
open Pp
open Util
open Names
@@ -642,29 +642,30 @@ let rec get_modtype_substobjs env = function
(subst_key (map_msid msid mp) sub_alias)
(map_msid msid mp)
| _ -> sub_alias in
- let sub3=
+ let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+ let mbid,mbids= (match mbids with
+ | mbid::mbids -> mbid,mbids
+ | [] -> match mexpr with
+ | MSEident _ -> error "Application of a non-functor"
+ | _ -> error "Application of a functor with too few arguments") in
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
+ let sub3=
if sub1 = empty_subst then
- update_subst sub_alias (map_mbid farg_id mp None)
+ update_subst sub_alias (map_mbid farg_id mp (Some resolve))
else
- let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
let sub_alias' = update_subst sub_alias sub1' in
join sub1' sub_alias'
in
- let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
- let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
- (match mbids with
- | mbid::mbids ->
- let resolve =
- Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
- | MSEident _ -> error "Application of a non-functor"
- | _ -> error "Application of a functor with too few arguments")
+ let sub3 = join sub3
+ (update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
+ , mbids, msid, objs)
| MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
@@ -948,30 +949,32 @@ let rec get_module_substobjs env = function
(subst_key (map_msid msid mp) sub_alias)
(map_msid msid mp)
| _ -> sub_alias in
-
+ let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+ let mbid,mbids =
+ (match mbids with
+ | mbid::mbids ->mbid,mbids
+
+ | [] -> match mexpr with
+ | MSEident _ -> error "Application of a non-functor"
+ | _ -> error "Application of a functor with too few arguments") in
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
let sub3=
if sub1 = empty_subst then
- update_subst sub_alias (map_mbid farg_id mp None)
+ update_subst sub_alias (map_mbid farg_id mp (Some resolve))
else
- let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
let sub_alias' = update_subst sub_alias sub1' in
- join sub1' sub_alias'
+ join sub1' sub_alias'
in
- let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
- let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
- (match mbids with
- | mbid::mbids ->
- let resolve =
- Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
- | MSEident _ -> error "Application of a non-functor"
- | _ -> error "Application of a functor with too few arguments")
+ let sub3 = join sub3 (update_subst sub_alias
+ (map_mbid farg_id mp (Some resolve))) in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
+ , mbids, msid, objs)
| MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
| MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
@@ -1061,12 +1064,9 @@ let rec update_include (sub,mbids,msid,objs) =
| (id,obj)::tail ->
if object_tag obj = "INCLUDE" then
let ((me,is_mod),substobjs,substituted) = out_include obj in
- if not (is_mod) then
- let substobjs' = update_include substobjs in
- (id, in_include ((me,true),substobjs',substituted))::
- (replace_include tail)
- else
- (id,obj)::(replace_include tail)
+ let substobjs' = update_include substobjs in
+ (id, in_include ((me,true),substobjs',substituted))::
+ (replace_include tail)
else
(id,obj)::(replace_include tail)
in
@@ -1142,7 +1142,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
| _ ->
let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
let (sub,mbids,msid,objs) = substobjs in
- let sub' = subst_key (map_msid msid mp) sub in
+ let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
let substobjs = (join sub sub',mbids,msid,objs) in
let substituted = subst_substobjs dir mp substobjs in
ignore (add_leaf
diff --git a/library/impargs.ml b/library/impargs.ml
index 2b2c607c..14f88728 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Util
open Names
@@ -26,8 +26,7 @@ open Termops
(*s Flags governing the computation of implicit arguments *)
type implicits_flags = {
- main : bool;
- manual : bool; (* automatic or manual only *)
+ auto : bool; (* automatic or manual only *)
strict : bool; (* true = strict *)
strongly_strict : bool; (* true = strongly strict *)
reversible_pattern : bool;
@@ -38,8 +37,7 @@ type implicits_flags = {
(* les implicites sont stricts par défaut en v8 *)
let implicit_args = ref {
- main = false;
- manual = false;
+ auto = false;
strict = true;
strongly_strict = false;
reversible_pattern = false;
@@ -48,11 +46,7 @@ let implicit_args = ref {
}
let make_implicit_args flag =
- implicit_args := { !implicit_args with main = flag }
-
-let make_manual_implicit_args flag =
- implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
- manual = flag }
+ implicit_args := { !implicit_args with auto = flag }
let make_strict_implicit_args flag =
implicit_args := { !implicit_args with strict = flag }
@@ -69,9 +63,7 @@ let make_contextual_implicit_args flag =
let make_maximal_implicit_args flag =
implicit_args := { !implicit_args with maximal = flag }
-let is_implicit_args () = !implicit_args.main
-let is_manual_implicit_args () = !implicit_args.manual
-let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ())
+let is_implicit_args () = !implicit_args.auto
let is_strict_implicit_args () = !implicit_args.strict
let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -316,10 +308,10 @@ let const v _ = v
let compute_implicits_auto env f manual t =
match manual with
| [] ->
- let l = compute_implicits_flags env f false t in
- if f.manual then List.map (const None) l
- else prepare_implicits f l
- | _ -> compute_manual_implicits env f t (not f.manual) manual
+ if not f.auto then []
+ else let l = compute_implicits_flags env f false t in
+ prepare_implicits f l
+ | _ -> compute_manual_implicits env f t f.auto manual
let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
@@ -523,7 +515,7 @@ let rebuild_implicits (req,l) =
| ImplManual m ->
let oldimpls = snd (List.hd l) in
let auto =
- if flags.main then
+ if flags.auto then
let newimpls = compute_global_implicits flags [] ref in
merge_impls oldimpls newimpls
else oldimpls
@@ -549,32 +541,30 @@ let declare_implicits_gen req flags ref =
add_anonymous_leaf (inImplicits (req,[ref,imps]))
let declare_implicits local ref =
- let flags = { !implicit_args with main = true } in
+ let flags = { !implicit_args with auto = true } in
let req =
if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
- declare_implicits_gen req flags ref
-
+ declare_implicits_gen req flags ref
+
let declare_var_implicits id =
- if !implicit_args.main then
- declare_implicits_gen ImplLocal !implicit_args (VarRef id)
+ let flags = !implicit_args in
+ declare_implicits_gen ImplLocal flags (VarRef id)
let declare_constant_implicits con =
- if !implicit_args.main then
- let flags = !implicit_args in
+ let flags = !implicit_args in
declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con)
let declare_mib_implicits kn =
- if !implicit_args.main then
- let flags = !implicit_args in
- let imps = array_map_to_list
- (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
- (compute_mib_implicits flags [] kn) in
+ let flags = !implicit_args in
+ let imps = array_map_to_list
+ (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
+ (compute_mib_implicits flags [] kn) in
add_anonymous_leaf
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
-
+
(* Declare manual implicits *)
type manual_explicitation = Topconstr.explicitation * (bool * bool)
-
+
let compute_implicits_with_manual env typ enriching l =
compute_manual_implicits env !implicit_args typ enriching l
@@ -582,7 +572,7 @@ let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let t = Global.type_of_global ref in
- let enriching = Option.default (is_auto_implicit_args ()) enriching in
+ let enriching = Option.default flags.auto enriching in
let l' = compute_manual_implicits env flags t enriching l in
let req =
if local or isVarRef ref then ImplLocal
diff --git a/library/impargs.mli b/library/impargs.mli
index a363effa..c1f119e6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: impargs.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Names
@@ -20,7 +20,6 @@ open Nametab
are outside the kernel, which knows nothing about implicit arguments. *)
val make_implicit_args : bool -> unit
-val make_manual_implicit_args : bool -> unit
val make_strict_implicit_args : bool -> unit
val make_strongly_strict_implicit_args : bool -> unit
val make_reversible_pattern_implicit_args : bool -> unit
@@ -28,7 +27,6 @@ val make_contextual_implicit_args : bool -> unit
val make_maximal_implicit_args : bool -> unit
val is_implicit_args : unit -> bool
-val is_manual_implicit_args : unit -> bool
val is_strict_implicit_args : unit -> bool
val is_strongly_strict_implicit_args : unit -> bool
val is_reversible_pattern_implicit_args : unit -> bool
diff --git a/library/lib.ml b/library/lib.ml
index 88bcd0b8..4a124cec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -452,7 +452,7 @@ type variable_context = variable_info list
type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
let sectab =
- ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
+ ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
let add_section () =
sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -460,13 +460,19 @@ let add_section () =
let add_section_variable id impl keep =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
- | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
+ | (vars,repl,abs)::sl ->
+ sectab := ((id,impl,keep)::vars,repl,abs)::sl
-let rec extract_hyps = function
- | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
- | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
- | (id::idl,hyps) -> extract_hyps (idl,hyps)
- | [], _ -> []
+let extract_hyps (secs,ohyps) =
+ let rec aux = function
+ | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
+ | ((id,impl,Some (ty,keep))::idl,hyps) ->
+ if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
+ (id,impl,None,ty) :: aux (idl,hyps)
+ else aux (idl,hyps)
+ | (id::idl,hyps) -> aux (idl,hyps)
+ | [], _ -> []
+ in aux (secs,ohyps)
let instance_from_variable_context sign =
let rec inst_rec = function
diff --git a/library/lib.mli b/library/lib.mli
index 23af7c17..dacfed59 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lib.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*s This module provides a general mechanism to keep a trace of all operations
@@ -182,7 +182,9 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
val section_instance : Libnames.global_reference -> Names.identifier array
val is_in_section : Libnames.global_reference -> bool
-val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit
+val add_section_variable : Names.identifier -> binding_kind ->
+ (Term.types * Names.identifier list) option -> unit
+
val add_section_constant : Names.constant -> Sign.named_context -> unit
val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
val replacement_context : unit ->
diff --git a/library/states.ml b/library/states.ml
index 7f7fef47..c81f9614 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *)
+(* $Id: states.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
open System
@@ -35,3 +35,10 @@ let with_heavy_rollback f x =
f x
with reraise ->
(unfreeze st; raise reraise)
+
+let with_state_protection f x =
+ let st = freeze () in
+ try
+ let a = f x in unfreeze st; a
+ with reraise ->
+ (unfreeze st; raise reraise)
diff --git a/library/states.mli b/library/states.mli
index eff046ef..210e06b2 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: states.mli 12080 2009-04-11 16:56:20Z herbelin $ i*)
(*s States of the system. In that module, we provide functions to get
and set the state of the whole system. Internally, it is done by
@@ -26,4 +26,9 @@ val unfreeze : state -> unit
val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+(*s [with_state_protection f x] applies [f] to [x] and restores the
+ state of the whole system as it was before the evaluation of f *)
+
+val with_state_protection : ('a -> 'b) -> 'a -> 'b
+
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7bebf6db..ad093507 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *)
+(* $Id: g_tactic.ml4 12009 2009-03-23 22:55:37Z herbelin $ *)
open Pp
open Pcoq
@@ -72,15 +72,16 @@ let test_lpar_id_colon =
let check_for_coloneq =
Gram.Entry.of_parser "lpar_id_colon"
(fun strm ->
- let rec skip_to_rpar n =
+ let rec skip_to_rpar p n =
match list_last (Stream.npeek n strm) with
- | ("",")") -> n+1
+ | ("","(") -> skip_to_rpar (p+1) (n+1)
+ | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
| ("",".") -> raise Stream.Failure
- | _ -> skip_to_rpar (n+1) in
+ | _ -> skip_to_rpar p (n+1) in
let rec skip_names n =
match list_last (Stream.npeek n strm) with
| ("IDENT",_) | ("","_") -> skip_names (n+1)
- | ("",":") -> skip_to_rpar (n+1) (* skip a constr *)
+ | ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *)
| _ -> raise Stream.Failure in
let rec skip_binders n =
match list_last (Stream.npeek n strm) with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f960492e..b2d67e1c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmo" i*)
-(* $Id: g_vernac.ml4 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
@@ -447,10 +447,13 @@ GEXTEND Gram
CWith_Module (fqid,qid)
] ]
;
- module_type:
+ module_type_atom:
[ [ qid = qualid -> CMTEident qid
-(* ... *)
- | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me)
+ | mty = module_type_atom; me = module_expr_atom -> CMTEapply (mty,me)
+ ] ]
+ ;
+ module_type:
+ [ [ mty = module_type_atom -> mty
| mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
] ]
;
@@ -700,7 +703,8 @@ GEXTEND Gram
| IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
| IDENT "Implicit"; qid = global -> PrintImplicit qid
| IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
- | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
+ | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
+ | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
;
class_rawexpr:
[ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d0a9c3d8..d2d81cd1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
-(*i $Id: pcoq.ml4 11784 2009-01-14 11:36:32Z herbelin $ i*)
+(*i $Id: pcoq.ml4 12055 2009-04-07 18:19:05Z herbelin $ i*)
open Pp
open Util
@@ -735,7 +735,10 @@ let is_binder_level from e =
let rec symbol_of_production assoc from forpat typ =
if is_binder_level from typ then
- Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
+ if forpat then
+ Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200")
+ else
+ Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
else if is_self from typ then
Gramext.Sself
else
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 78c63ca2..5f4ea5a6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ppvernac.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: ppvernac.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Names
@@ -897,7 +897,8 @@ let rec pr_vernac = function
| PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid
(* spiwack: command printing all the axioms and section variables used in a
term *)
- | PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+ | PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+ ++spc()++pr_reference qid
in pr_printable p
| VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
| VernacLocate loc ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5543a31c..1e50bc51 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 11622 2008-11-23 08:45:56Z herbelin $ *)
+(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -107,8 +107,9 @@ let need_expansion impl ref =
let typ = Global.type_of_global ref in
let ctx = fst (decompose_prod_assum typ) in
let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
- impl <> [] & let _,lastimpl = list_chop nprods impl in
- List.filter is_status_implicit lastimpl <> []
+ impl <> [] & List.length impl >= nprods &
+ let _,lastimpl = list_chop nprods impl in
+ List.filter is_status_implicit lastimpl <> []
type opacity =
| FullyOpaque
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 10034dd9..0c673fbd 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: printer.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -431,10 +431,11 @@ let pr_prim_rule = function
(str"cut " ++ pr_constr t ++
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
- | FixRule (f,n,[]) ->
+ | FixRule (f,n,[],_) ->
(str"fix " ++ pr_id f ++ str"/" ++ int n)
- | FixRule (f,n,others) ->
+ | FixRule (f,n,others,j) ->
+ if j<>0 then warning "Unsupported printing of \"fix\"";
let rec print_mut = function
| (f,n,ar)::oth ->
pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -442,10 +443,11 @@ let pr_prim_rule = function
(str"fix " ++ pr_id f ++ str"/" ++ int n ++
str" with " ++ print_mut others)
- | Cofix (f,[]) ->
+ | Cofix (f,[],_) ->
(str"cofix " ++ pr_id f)
- | Cofix (f,others) ->
+ | Cofix (f,others,j) ->
+ if j<>0 then warning "Unsupported printing of \"fix\"";
let rec print_mut = function
| (f,ar)::oth ->
(pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
@@ -499,10 +501,10 @@ let pr_assumptionset env s =
if (Environ.ContextObjectMap.is_empty s) then
str "Closed under the global context"
else
- let (vars,axioms) =
- Environ.ContextObjectMap.fold (fun o typ r ->
- let (v,a) = r in
- match o with
+ let (vars,axioms,opaque) =
+ Environ.ContextObjectMap.fold (fun t typ r ->
+ let (v,a,o) = r in
+ match t with
| Variable id -> ( Some (
Option.default (fnl ()) v
++ str (string_of_id id)
@@ -511,7 +513,7 @@ let pr_assumptionset env s =
++ fnl ()
)
,
- a )
+ a, o)
| Axiom kn -> ( v ,
Some (
Option.default (fnl ()) a
@@ -520,16 +522,28 @@ let pr_assumptionset env s =
++ pr_ltype typ
++ fnl ()
)
+ , o
)
- )
- s (None,None)
+ | Opaque kn -> ( v , a ,
+ Some (
+ Option.default (fnl ()) o
+ ++ (pr_constant env kn)
+ ++ str " : "
+ ++ pr_ltype typ
+ ++ fnl ()
+ )
+ )
+ )
+ s (None,None,None)
in
- let (vars,axioms) =
+ let (vars,axioms,opaque) =
( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
- Option.map (fun p -> str "Axioms:" ++ p) axioms
+ Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+ Option.map (fun p -> str "Opaque constants:" ++ p) opaque
)
in
(Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+ ++ (Option.default (mt ()) opaque)
let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4880f5e..c2d8921e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
open Util
open Names
@@ -130,7 +130,7 @@ let push_rel_defs =
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
let rec regeneralize_index i k t = match kind_of_term t with
| Rel j when j = i+k -> mkRel (k+1)
@@ -605,19 +605,13 @@ let find_dependencies_signature deps_in_rhs typs =
let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
List.map (fun (_,deps,_) -> deps) l
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+ and xn:Tn has just been regeneralized into x:Tn so that the terms
+ to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
-(* A Pushed term to match has just been substituted by some
- constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
- match
-
- - all terms to match and to push (dependent on t by definition)
- must have (Rel depth) substituted by t and Rel's>depth lifted by n
- - all pushed terms to match (non dependent on t by definition) must
- be lifted by n
-
- We start with depth=1
-*)
+ [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+ former references to xn are now references to x. Note that t1..tq
+ are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
let regeneralize_index_tomatch n =
let rec genrec depth = function
@@ -661,6 +655,13 @@ let replace_tomatch n c =
let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+ some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+ added to match; all pushed terms to match must be lifted by n
+ (knowing that [Abstract] introduces a binder in the list of pushed
+ terms to match).
+*)
+
let rec liftn_tomatch_stack n depth = function
| [] -> []
| Pushed ((c,tm),l,dep)::rest ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4c5ebe3e..043a326d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
open Pp
open Util
@@ -474,11 +474,11 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
let (evd',ks,_) =
List.fold_left
(fun (i,ks,m) b ->
- if m=0 then (i,t2::ks, n-1) else
+ if m=n then (i,t2::ks, m-1) else
let dloc = (dummy_loc,InternalHole) in
let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
- (i', ev :: ks, n - 1))
- (evd,[],n) bs
+ (i', ev :: ks, m - 1))
+ (evd,[],List.length bs - 1) bs
in
ise_and evd'
[(fun i ->
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
if is_defined_evar i ev1 then
evar_conv_x env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+ solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c0c0b941..994da427 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
open Util
open Pp
@@ -673,7 +673,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
- invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+ let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+ match res with
+ | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+ | _ -> res
+
let effective_projections =
map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -836,7 +840,7 @@ let expand_rhs env sigma subst rhs =
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress
-let rec invert_definition env evd (evk,argsv as ev) rhs =
+let rec invert_definition choose env evd (evk,argsv as ev) rhs =
let evdref = ref evd in
let progress = ref false in
let evi = Evd.find (evars_of evd) evk in
@@ -847,7 +851,11 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
try
let sols = find_projectable_vars true env (evars_of !evdref) t subst in
- let c, p = filter_solution sols in
+ let c, p = match sols with
+ | [] -> raise Not_found
+ | [id,p] -> (mkVar id, p)
+ | (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+ in
let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
let evd = do_projection_effects evar_define env ty !evdref p in
evdref := evd;
@@ -923,9 +931,9 @@ and occur_existential evm c =
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-and evar_define env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
try
- let (evd',body) = invert_definition env evd ev rhs in
+ let (evd',body) = invert_definition choose env evd ev rhs in
if occur_meta body then error "Meta cannot occur in evar body.";
(* invert_definition may have instantiate some evars of rhs with evk *)
(* so we recheck acyclicity *)
@@ -1120,7 +1128,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
* if the problem couldn't be solved. *)
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
try
let t2 = whd_evar (evars_of evd) t2 in
let evd = match kind_of_term t2 with
@@ -1132,15 +1140,18 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
then solve_evar_evar evar_define env evd ev1 ev2
else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
| _ ->
- let evd = evar_define env ev1 t2 evd in
+ let evd = evar_define ~choose env ev1 t2 evd in
let evm = evars_of evd in
let evi = Evd.find evm evk1 in
if occur_existential evm evi.evar_concl then
let evenv = evar_env evi in
let evc = nf_isevar evd evi.evar_concl in
- let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
- let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
- add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+ match evi.evar_body with
+ | Evar_defined body ->
+ let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
+ add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+ | Evar_empty -> (* Resulted in a constraint *)
+ evd
else evd
in
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
@@ -1251,8 +1262,8 @@ let define_evar_as_abstraction abs evd (ev,args) =
let evrng =
fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
- (evd3,prod')
-
+ (evd3,prod')
+
let define_evar_as_product evd (ev,args) =
define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
@@ -1263,7 +1274,6 @@ let define_evar_as_sort evd (ev,args) =
let s = new_Type () in
Evd.evar_define ev s evd, destSort s
-
(* We don't try to guess in which sort the type should be defined, since
any type has type Type. May cause some trouble, but not so far... *)
@@ -1275,27 +1285,26 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
an evar instantiate it with the product of 2 new evars. *)
let split_tycon loc env evd tycon =
- let rec real_split c =
- let sigma = evars_of evd in
- let t = whd_betadeltaiota env sigma c in
+ let rec real_split evd c =
+ let t = whd_betadeltaiota env (Evd.evars_of evd) c in
match kind_of_term t with
| Prod (na,dom,rng) -> evd, (na, dom, rng)
| Evar ev when not (Evd.is_defined_evar evd ev) ->
let (evd',prod) = define_evar_as_product evd ev in
let (_,dom,rng) = destProd prod in
evd',(Anonymous, dom, rng)
- | _ -> error_not_product_loc loc env sigma c
+ | _ -> error_not_product_loc loc env (Evd.evars_of evd) c
in
match tycon with
| None -> evd,(Anonymous,None,None)
| Some (abs, c) ->
(match abs with
None ->
- let evd', (n, dom, rng) = real_split c in
+ let evd', (n, dom, rng) = real_split evd c in
evd', (n, mk_tycon dom, mk_tycon rng)
| Some (init, cur) ->
if cur = 0 then
- let evd', (x, dom, rng) = real_split c in
+ let evd', (x, dom, rng) = real_split evd c in
evd, (Anonymous,
Some (None, dom),
Some (None, rng))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a687fdf0..cb54f400 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
(*i*)
open Util
@@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
(***********************************************************)
(* Instantiate evars *)
-(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
- some problems that cannot be solved in a unique way;
- failed if the instance is not valid for the given [ev] *)
-val evar_define : env -> existential -> constr -> evar_defs -> evar_defs
+ some problems that cannot be solved in a unique way (except if choose is
+ true); fails if the instance is not valid for the given [ev] *)
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
(***********************************************************)
(* Evars/Metas switching... *)
@@ -80,7 +80,7 @@ val solve_refl :
evar_defs
val solve_simple_eqn :
(env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
- -> env -> evar_defs -> conv_pb * existential * constr ->
+ -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr ->
evar_defs * bool
(* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1cac9011..c0f820a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
open Pp
open Util
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref resj tycon
| RLetIn(loc,name,c1,c2) ->
- let j = pretype empty_tycon env evdref lvar c1 in
+ let j =
+ match c1 with
+ | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+ let tj = pretype_type empty_valcon env evdref lvar t in
+ pretype (mk_tycon tj.utj_val) env evdref lvar c
+ | _ -> pretype empty_tycon env evdref lvar c1
+ in
let t = refresh_universes j.uj_type in
let var = (name,Some j.uj_val,t) in
let tycon = lift_tycon 1 tycon in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c4023b9..711f332e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: recordops.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Util
open Pp
@@ -65,8 +65,11 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
if projs' == projs && kn' == kn && id' == id then obj else
((kn',i),id',kl,projs')
+let discharge_constructor (ind, n) =
+ (Lib.discharge_inductive ind, n)
+
let discharge_structure (_,(ind,id,kl,projs)) =
- Some (Lib.discharge_inductive ind, id, kl,
+ Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
List.map (Option.map Lib.discharge_con) projs)
let (inStruc,outStruc) =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f93212f8..4f38fbb3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *)
open Pp
open Util
@@ -1017,6 +1017,15 @@ let assums_of_rel_context sign =
| None -> (na, t)::l)
sign ~init:[]
+let fold_map_rel_context f env sign =
+ let rec aux env acc = function
+ | d::sign ->
+ aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+ | [] ->
+ acc
+ in
+ aux env [] (List.rev sign)
+
let map_rel_context_with_binders f sign =
let rec aux k = function
| d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d44c762e..e0bbe7b5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: termops.mli 12058 2009-04-08 10:54:59Z herbelin $ i*)
open Util
open Pp
@@ -241,6 +241,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
val assums_of_rel_context : rel_context -> (name * constr) list
val lift_rel_context : int -> rel_context -> rel_context
val substl_rel_context : constr list -> rel_context -> rel_context
+val fold_map_rel_context :
+ (env -> constr -> constr) -> env -> rel_context -> rel_context
val map_rel_context_with_binders :
(int -> constr -> constr) -> rel_context -> rel_context
val fold_named_context_both_sides :
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8680e578..216a0611 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*)
(*i*)
open Names
@@ -381,7 +381,7 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
if not (has_typeclasses (Evd.evars_of evd)) then evd
else
- !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+ !solve_instanciations_problem env evd onlyargs split fail
let resolve_one_typeclass env evm t =
!solve_instanciation_problem env evm t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fb29196c..bfd601e2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
open Pp
open Util
@@ -492,7 +492,7 @@ let w_coerce env evd mv c =
let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
- let t = get_type_of_with_meta env sigma (metas_of evd) c in
+ let t = get_type_of_with_meta env sigma (List.map (on_snd (nf_meta evd)) (metas_of evd)) (nf_meta evd c) in
let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
@@ -500,7 +500,7 @@ let unify_to_type env evd flags c u =
let unify_type env evd flags mv c =
let mvty = Typing.meta_type evd mv in
- if occur_meta_or_existential mvty then
+ if occur_meta_or_existential mvty or is_arity env (evars_of evd) mvty then
unify_to_type env evd flags c mvty
else ([],[])
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f5204be5..769a9572 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenvtac.ml 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: clenvtac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
open Pp
open Util
@@ -25,7 +25,6 @@ open Logic
open Reduction
open Reductionops
open Tacmach
-open Evar_refiner
open Rawterm
open Pattern
open Tacexpr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d19d81e0..f4613f8d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: evar_refiner.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
open Util
open Names
@@ -15,6 +15,7 @@ open Evd
open Sign
open Proof_trees
open Refiner
+open Pretyping
(******************************************)
(* Instantiation of existential variables *)
@@ -22,21 +23,21 @@ open Refiner
(* w_tactic pour instantiate *)
-let w_refine evk rawc evd =
+let w_refine evk (ltac_vars,rawc) evd =
if Evd.is_defined (evars_of evd) evk then
error "Instantiate called on already-defined evar";
let e_info = Evd.find (evars_of evd) evk in
let env = Evd.evar_env e_info in
- let sigma,typed_c =
- try Pretyping.Default.understand_tcc ~resolve_classes:false
- (evars_of evd) env ~expected_type:e_info.evar_concl rawc
+ let evd',typed_c =
+ try Pretyping.Default.understand_ltac
+ (evars_of evd) env ltac_vars (OfType (Some e_info.evar_concl)) rawc
with _ ->
let loc = Rawterm.loc_of_rawconstr rawc in
user_err_loc
(loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
string_of_existential evk))
in
- evar_define evk typed_c (evars_reset_evd sigma evd)
+ evar_define evk typed_c (evars_reset_evd (evars_of evd') evd)
(* vernac command Existential *)
@@ -55,5 +56,5 @@ let instantiate_pf_com n com pfts =
let env = Evd.evar_env evi in
let rawc = Constrintern.intern_constr sigma env com in
let evd = create_goal_evar_defs sigma in
- let evd' = w_refine evk rawc evd in
+ let evd' = w_refine evk (([],[]),rawc) evd in
change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index baa6b19a..a42b11a4 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evar_refiner.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: evar_refiner.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
(*i*)
open Names
@@ -14,11 +14,14 @@ open Term
open Environ
open Evd
open Refiner
+open Pretyping
+open Rawterm
(*i*)
(* Refinement of existential variables. *)
-val w_refine : evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
+val w_refine : evar -> (var_map * unbound_ltac_var_map) * rawconstr ->
+ evar_defs -> evar_defs
val instantiate_pf_com :
int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3e758eb6..caf6f56b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
open Pp
open Util
@@ -517,7 +517,7 @@ let prim_refiner r sigma goal =
let sg2 = mk_goal sign cl in
if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
- | FixRule (f,n,rest) ->
+ | FixRule (f,n,rest,j) ->
let rec check_ind env k cl =
match kind_of_term (strip_outer_cast cl) with
| Prod (na,c1,b) ->
@@ -531,7 +531,8 @@ let prim_refiner r sigma goal =
| _ -> error "Not enough products."
in
let (sp,_) = check_ind env n cl in
- let all = (f,n,cl)::rest in
+ let firsts,lasts = list_chop j rest in
+ let all = firsts@(f,n,cl)::lasts in
let rec mk_sign sign = function
| (f,n,ar)::oth ->
let (sp',_) = check_ind env n ar in
@@ -539,14 +540,15 @@ let prim_refiner r sigma goal =
error ("Fixpoints should be on the same " ^
"mutual inductive declaration.");
if !check && mem_named_context f (named_context_of_val sign) then
- error "Name already used in the environment";
+ error
+ ("Name "^string_of_id f^" already used in the environment");
mk_sign (push_named_context_val (f,None,ar) sign) oth
| [] ->
List.map (fun (_,_,c) -> mk_goal sign c) all
in
(mk_sign sign all, sigma)
- | Cofix (f,others) ->
+ | Cofix (f,others,j) ->
let rec check_is_coind env cl =
let b = whd_betadeltaiota env sigma cl in
match kind_of_term b with
@@ -558,7 +560,8 @@ let prim_refiner r sigma goal =
error ("All methods must construct elements " ^
"in coinductive types.")
in
- let all = (f,cl)::others in
+ let firsts,lasts = list_chop j others in
+ let all = firsts@(f,cl)::lasts in
List.iter (fun (_,c) -> check_is_coind env c) all;
let rec mk_sign sign = function
| (f,ar)::oth ->
@@ -687,24 +690,26 @@ let prim_extractor subfun vl pft =
mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
subfun (add_proof_var id vl) spf2)
- | Some (Prim (FixRule (f,n,others)),spfl) ->
- let all = Array.of_list ((f,n,cl)::others) in
+ | Some (Prim (FixRule (f,n,others,j)),spfl) ->
+ let firsts,lasts = list_chop j others in
+ let all = Array.of_list (firsts@(f,n,cl)::lasts) in
let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
let names = Array.map (fun (f,_,_) -> Name f) all in
let vn = Array.map (fun (_,n,_) -> n-1) all in
let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
(add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkFix ((vn,0),(names,lcty,lfix))
+ mkFix ((vn,j),(names,lcty,lfix))
- | Some (Prim (Cofix (f,others)),spfl) ->
- let all = Array.of_list ((f,cl)::others) in
+ | Some (Prim (Cofix (f,others,j)),spfl) ->
+ let firsts,lasts = list_chop j others in
+ let all = Array.of_list (firsts@(f,cl)::lasts) in
let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
let names = Array.map (fun (f,_) -> Name f) all in
let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
(add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkCoFix (0,(names,lcty,lfix))
+ mkCoFix (j,(names,lcty,lfix))
| Some (Prim (Refine c),spfl) ->
let mvl = collect_meta_variables c in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1e673853..150fb89f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_type.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(*i $Id: proof_type.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
(*i*)
open Environ
@@ -29,8 +29,8 @@ open Pattern
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list
- | Cofix of identifier * (identifier * constr) list
+ | FixRule of identifier * int * (identifier * int * constr) list * int
+ | Cofix of identifier * (identifier * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 21cd8b28..c80e126f 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: proof_type.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: proof_type.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
(*i*)
open Environ
@@ -29,8 +29,8 @@ open Pattern
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list
- | Cofix of identifier * (identifier * constr) list
+ | FixRule of identifier * int * (identifier * int * constr) list * int
+ | Cofix of identifier * (identifier * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6c4f7b5e..b740baa8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
open Pp
open Util
@@ -211,11 +211,15 @@ let rec rename_hyp_no_check l gl = match l with
tclTHEN (refiner (Prim (Rename (id1,id2))))
(rename_hyp_no_check l) gl
-let mutual_fix f n others gl =
- with_check (refiner (Prim (FixRule (f,n,others)))) gl
+let mutual_fix_with_index f n others j gl =
+ with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
-let mutual_cofix f others gl =
- with_check (refiner (Prim (Cofix (f,others)))) gl
+let mutual_fix f n others = mutual_fix_with_index f n others 0
+
+let mutual_cofix_with_index f others j gl =
+ with_check (refiner (Prim (Cofix (f,others,j)))) gl
+
+let mutual_cofix f others = mutual_cofix_with_index f others 0
(* Versions with consistency checks *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cdcb8bfd..37acf850 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: tacmach.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
(*i*)
open Names
@@ -137,6 +137,10 @@ val order_hyps : identifier list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
+val mutual_fix_with_index :
+ identifier -> int -> (identifier * int * constr) list -> int -> tactic
+val mutual_cofix_with_index :
+ identifier -> (identifier * constr) list -> int -> tactic
(*s The most primitive tactics with consistency and type checking *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1212656b..36136a6c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: auto.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -150,10 +150,13 @@ module Hint_db = struct
try Constr_map.find key db.hintdb_map
with Not_found -> empty_se
+ let map_none db =
+ Sort.merge pri_order db.hintdb_nopat []
+
let map_all k db =
let (l,l',_) = find k db in
Sort.merge pri_order (db.hintdb_nopat @ l) l'
-
+
let map_auto (k,c) db =
let st = if db.use_dn then Some db.hintdb_state else None in
let l' = lookup_tacs (k,c) st (find k db) in
@@ -637,26 +640,24 @@ let print_hint_ref ref = ppnl(pr_hint_ref ref)
let pr_hint_term cl =
try
- let (hdc,args) = head_constr_bound cl in
- let hd = head_of_constr_reference hdc in
let dbs = Hintdbmap.to_list !searchtable in
let valid_dbs =
- if occur_existential cl then
- map_succeed
- (fun (name, db) -> (name, db, Hint_db.map_all hd db))
- dbs
- else
- map_succeed
- (fun (name, db) ->
- (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db))
- dbs
- in
- if valid_dbs = [] then
- (str "No hint applicable for current goal")
- else
- (str "Applicable Hints :" ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
- with Bound | Match_failure _ | Failure _ ->
+ let fn = try
+ let (hdc,args) = head_constr_bound cl in
+ let hd = head_of_constr_reference hdc in
+ if occur_existential cl then
+ Hint_db.map_all hd
+ else Hint_db.map_auto (hd, applist (hdc,args))
+ with Bound -> Hint_db.map_none
+ in
+ map_succeed (fun (name, db) -> (name, db, fn db)) dbs
+ in
+ if valid_dbs = [] then
+ (str "No hint applicable for current goal")
+ else
+ (str "Applicable Hints :" ++ fnl () ++
+ hov 0 (prlist pr_hints_db valid_dbs))
+ with Match_failure _ | Failure _ ->
(str "No hint applicable for current goal")
let error_no_such_hint_database x =
@@ -795,6 +796,13 @@ let flags_of_state st =
{auto_unif_flags with
modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+let hintmap_of hdc concl =
+ match hdc with
+ | None -> Hint_db.map_none
+ | Some hdc ->
+ if occur_existential concl then Hint_db.map_all hdc
+ else Hint_db.map_auto (hdc,concl)
+
let rec trivial_fail_db mod_delta db_list local_db gl =
let intro_tac =
tclTHEN intro
@@ -808,12 +816,8 @@ let rec trivial_fail_db mod_delta db_list local_db gl =
(trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
and my_find_search_nodelta db_list local_db hdc concl =
- if occur_existential concl then
- List.map (fun hint -> (None,hint))
- (list_map_append (Hint_db.map_all hdc) (local_db::db_list))
- else
- List.map (fun hint -> (None,hint))
- (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list))
+ List.map (fun hint -> (None,hint))
+ (list_map_append (hintmap_of hdc concl) (local_db::db_list))
and my_find_search mod_delta =
if mod_delta then my_find_search_delta
@@ -821,28 +825,31 @@ and my_find_search mod_delta =
and my_find_search_delta db_list local_db hdc concl =
let flags = {auto_unif_flags with use_metas_eagerly = true} in
+ let f = hintmap_of hdc concl in
if occur_existential concl then
list_map_append
(fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+ List.map (fun x -> (Some flags,x)) (f db)
else
let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
- List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db))
+ List.map (fun x -> (Some flags,x)) (f db))
(local_db::db_list)
else
list_map_append (fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db)
+ List.map (fun x -> (Some flags, x)) (f db)
else
let (ids, csts as st) = Hint_db.transparent_state db in
let flags, l =
let l =
- if (Idpred.is_empty ids && Cpred.is_empty csts)
- then Hint_db.map_auto (hdc,concl) db
- else Hint_db.map_all hdc db
+ match hdc with None -> Hint_db.map_none db
+ | Some hdc ->
+ if (Idpred.is_empty ids && Cpred.is_empty csts)
+ then Hint_db.map_auto (hdc,concl) db
+ else Hint_db.map_all hdc db
in {flags with modulo_delta = st}, l
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
@@ -861,13 +868,15 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
and trivial_resolve mod_delta db_list local_db cl =
try
- let hdconstr,_ = head_constr_bound cl in
- List.map (tac_of_hint db_list local_db cl)
- (priority
- (my_find_search mod_delta db_list local_db
- (head_of_constr_reference hdconstr) cl))
- with Bound | Not_found ->
- []
+ let head =
+ try let hdconstr,_ = head_constr_bound cl in
+ Some (head_of_constr_reference hdconstr)
+ with Bound -> None
+ in
+ List.map (tac_of_hint db_list local_db cl)
+ (priority
+ (my_find_search mod_delta db_list local_db head cl))
+ with Not_found -> []
let trivial lems dbnames gl =
let db_list =
@@ -903,12 +912,14 @@ let h_trivial lems l =
let possible_resolve mod_delta db_list local_db cl =
try
- let hdconstr,_ = head_constr_bound cl in
- List.map (tac_of_hint db_list local_db cl)
- (my_find_search mod_delta db_list local_db
- (head_of_constr_reference hdconstr) cl)
- with Bound | Not_found ->
- []
+ let head =
+ try let hdconstr,_ = head_constr_bound cl in
+ Some (head_of_constr_reference hdconstr)
+ with Bound -> None
+ in
+ List.map (tac_of_hint db_list local_db cl)
+ (my_find_search mod_delta db_list local_db head cl)
+ with Not_found -> []
let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index c9065ef3..132b9063 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id: auto.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Util
@@ -53,6 +53,7 @@ module Hint_db :
type t
val empty : transparent_state -> bool -> t
val find : global_reference -> t -> search_entry
+ val map_none : t -> pri_auto_tactic list
val map_all : global_reference -> t -> pri_auto_tactic list
val map_auto : global_reference * constr -> t -> pri_auto_tactic list
val add_one : hint_entry -> t -> t
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6a425984..b7eb3620 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: class_tactics.ml4 12189 2009-06-15 05:08:44Z msozeau $ *)
open Pp
open Util
@@ -46,18 +46,18 @@ let typeclasses_db = "typeclass_instances"
let _ = Auto.auto_init := (fun () ->
Auto.create_hint_db false typeclasses_db full_transparent_state true)
-let check_imported_library d =
+let check_required_library d =
let d' = List.map id_of_string d in
let dir = make_dirpath (List.rev d') in
if not (Library.library_is_loaded dir) then
- error ("Library "^(list_last d)^" has to be imported first.")
+ error ("Library "^(list_last d)^" has to be required first.")
let classes_dirpath =
make_dirpath (List.map id_of_string ["Classes";"Coq"])
let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
- else check_imported_library ["Coq";"Setoids";"Setoid"]
+ else check_required_library ["Coq";"Setoids";"Setoid"]
(** Typeclasses instance search tactic / eauto *)
@@ -245,7 +245,6 @@ module SearchProblem = struct
Option.iter (fun r ->
(* msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
r := true) do_cut;
- let sigma = Evarutil.nf_evars sigma in
let gl = List.map (Evarutil.nf_evar_info sigma) gl in
let nbgl = List.length gl in
(* let gl' = { it = gl ; sigma = sigma } in *)
@@ -338,6 +337,7 @@ let is_transparent_gr (ids, csts) = function
| IndRef _ | ConstructRef _ -> false
let make_resolve_hyp env sigma st flags pri (id, _, cty) =
+ let cty = Evarutil.nf_evar sigma cty in
let ctx, ar = decompose_prod cty in
let keep =
match kind_of_term (fst (decompose_app ar)) with
@@ -625,9 +625,6 @@ let is_applied_setoid_relation t =
let _ =
Equality.register_is_applied_setoid_relation is_applied_setoid_relation
-exception Found of (constr * constr * (types * types) list * constr * constr array *
- (constr * (constr * constr * constr * constr)) option array)
-
let split_head = function
hd :: tl -> hd, tl
| [] -> assert(false)
@@ -1675,7 +1672,7 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl =
let bindings = Tacinterp.interp_bindings my_ist gl bl in
typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type
-let typeclass_app_raw t gl =
+let typeclass_app_raw (_,t) gl =
let env = pf_env gl in
let evars = ref (create_evar_defs (project gl)) in
let j = Pretyping.Default.understand_judgment_tcc evars env t in
@@ -1715,7 +1712,7 @@ END
let not_declared env ty rel =
tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++
- str ty ++ str" relation. Maybe you need to import the Setoid library")
+ str ty ++ str" relation. Maybe you need to require the Setoid library")
let relation_of_constr env c =
match kind_of_term c with
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 2d0395a3..62a8ddfc 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *)
open Util
open Pp
@@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt =
let mark_as_done pts =
map_pftreestate
(fun _ -> mark_proof_tree_as_done)
- (traverse 0 pts)
+ (up_to_matching_rule is_focussing_command pts)
(* post-instruction focus management *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index baebee07..58a00419 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
open Pp
open Util
@@ -1215,7 +1215,7 @@ let subst_one x gl =
tclMAP introtac depdecls]) @
[tclTRY (clear [x;hyp])]) gl
-let subst = tclMAP subst_one
+let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
let subst_all gl =
let test (_,c) =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 43c18a8b..67b89888 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evar_tactics.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: evar_tactics.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
open Term
open Util
@@ -29,7 +29,7 @@ let evar_list evc c =
in
evrec [] c
-let instantiate n rawc ido gl =
+let instantiate n (ist,rawc) ido gl =
let sigma = gl.sigma in
let evl =
match ido with
@@ -52,7 +52,9 @@ let instantiate n rawc ido gl =
error "not enough uninstantiated existential variables";
if n <= 0 then error "Incorrect existential variable index.";
let ev,_ = destEvar (List.nth evl (n-1)) in
- let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
+ let env = Evd.evar_env (Evd.find sigma ev) in
+ let ltac_vars = Tacinterp.extract_ltac_vars ist sigma env in
+ let evd' = w_refine ev (ltac_vars,rawc) (create_goal_evar_defs sigma) in
tclTHEN
(tclEVARS (evars_of evd'))
tclNORMEVAR
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index cc06d2c6..f577b338 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,14 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: evar_tactics.mli 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id: evar_tactics.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
open Tacmach
open Names
open Tacexpr
open Termops
-val instantiate : int -> Rawterm.rawconstr ->
+val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr ->
(identifier * hyp_location_flag, unit) location -> tactic
(*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 694c3495..5eb333a0 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: extraargs.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: extraargs.ml4 12102 2009-04-24 10:48:11Z herbelin $ *)
open Pp
open Pcoq
@@ -100,9 +100,9 @@ END
let pr_gen prc _prlc _prtac c = prc c
-let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw
-let interp_raw _ _ (t,_) = t
+let interp_raw ist gl (t,_) = (ist,t)
let glob_raw = Tacinterp.intern_constr
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index bccb150f..b64adf24 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraargs.mli 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: extraargs.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
open Tacexpr
open Term
@@ -25,7 +25,7 @@ val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
val wit_occurrences : (int list) typed_abstract_argument_type
val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : rawconstr typed_abstract_argument_type
+val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type
val raw : constr_expr Pcoq.Gram.Entry.e
type 'id gen_place= ('id * hyp_location_flag,unit) location
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b270ba2d..8e517453 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
open Term
open Proof_type
@@ -75,10 +75,6 @@ let h_generalize_dep c =
let h_let_tac b na c cl =
let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
-let h_instantiate n c ido =
-(Evar_tactics.instantiate n c ido)
- (* abstract_tactic (TacInstantiate (n,c,cls))
- (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
(* Derived basic tactics *)
let h_simple_induction_destruct isrec h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 0ebb024a..9270411a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: hiddentac.mli 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
(*i*)
open Names
@@ -62,8 +62,6 @@ val h_generalize_gen : (constr with_occurrences * name) list -> tactic
val h_generalize_dep : constr -> tactic
val h_let_tac : letin_flag -> name -> constr ->
Tacticals.clause -> tactic
-val h_instantiate : int -> Rawterm.rawconstr ->
- (identifier * hyp_location_flag, unit) location -> tactic
(* Derived basic tactics *)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index dff3b003..322d25e5 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refine.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
(* JCF -- 6 janvier 1998 EXPERIMENTAL *)
@@ -327,29 +327,31 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
gl
(* fix => tactique Fix *)
- | Fix ((ni,_),(fi,ai,_)) , _ ->
+ | Fix ((ni,j),(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
+ let firsts,lasts = list_chop j (Array.to_list fixes) in
tclTHENS
- (mutual_fix (out_name fi.(0)) (succ ni.(0))
- (List.tl (Array.to_list fixes)))
+ (mutual_fix_with_index
+ (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
(* cofix => tactique CoFix *)
- | CoFix (_,(fi,ai,_)) , _ ->
+ | CoFix (j,(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
+ let firsts,lasts = list_chop j (Array.to_list cofixes) in
tclTHENS
- (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
+ (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j)
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
@@ -366,10 +368,15 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
(* Et finalement la tactique refine elle-même : *)
-let refine oc gl =
+let refine (evd,c) gl =
let sigma = project gl in
- let (sigma,c) = Evarutil.evars_to_metas sigma oc in
+ let evd = Evd.evars_of (Typeclasses.resolve_typeclasses
+ ~onlyargs:true ~fail:false (pf_env gl)
+ (Evd.create_evar_defs evd))
+ in
+ let c = Evarutil.nf_evar evd c in
+ let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
(* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
complicated to update meta types when passing through a binder *)
- let th = compute_metamap (pf_env gl) sigma c in
- tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl
+ let th = compute_metamap (pf_env gl) evd c in
+ tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9026a6d..71b50b66 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Constrintern
open Closure
@@ -539,7 +539,9 @@ let intern_induction_arg ist = function
| ElimOnIdent (loc,id) ->
if !strict_check then
(* If in a defined tactic, no intros-until *)
- ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings)
+ match intern_constr ist (CRef (Ident (dloc,id))) with
+ | RVar (loc,id),_ -> ElimOnIdent (loc,id)
+ | c -> ElimOnConstr (c,NoBindings)
else
ElimOnIdent (loc,id)
@@ -1396,6 +1398,14 @@ let retype_list sigma env lst =
try (x,Retyping.get_judgment_of env sigma csr)::a with
| Anomaly _ -> a) lst []
+let extract_ltac_vars_data ist sigma env =
+ let (ltacvars,_ as vars) = constr_list ist env in
+ vars, retype_list sigma env ltacvars
+
+let extract_ltac_vars ist sigma env =
+ let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
+ typs,unbndltacvars
+
let implicit_tactic = ref None
let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1441,8 +1451,8 @@ let solve_remaining_evars env initial_sigma evd c =
proc_rec (Evarutil.nf_isevar !evdref c)
let interp_gen kind ist sigma env (c,ce) =
- let (ltacvars,unbndltacvars as vars) = constr_list ist env in
- let typs = retype_list sigma env ltacvars in
+ let (ltacvars,unbndltacvars as vars),typs =
+ extract_ltac_vars_data ist sigma env in
let c = match ce with
| None -> c
(* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1717,10 +1727,20 @@ let interp_induction_arg ist gl = function
| ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c)
| ElimOnAnonHyp n as x -> x
| ElimOnIdent (loc,id) ->
- if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
- else ElimOnConstr
- (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
- NoBindings)
+ try
+ match List.assoc id ist.lfun with
+ | VInteger n -> ElimOnAnonHyp n
+ | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
+ | VConstr c -> ElimOnConstr (c,NoBindings)
+ | _ -> user_err_loc (loc,"",
+ strbrk "Cannot coerce " ++ pr_id id ++
+ strbrk " neither to a quantified hypothesis nor to a term.")
+ with Not_found ->
+ (* Interactive mode *)
+ if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id)
+ else ElimOnConstr
+ (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))),
+ NoBindings)
let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
@@ -2735,6 +2755,7 @@ let bad_tactic_args s =
(* Declaration of the TAC-DEFINITION object *)
let add (kn,td) = mactab := Gmap.add kn td !mactab
+let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
type tacdef_kind = | NewTac of identifier
| UpdateTac of ltac_constant
@@ -2749,9 +2770,7 @@ let load_md i ((sp,kn),defs) =
let kn = Names.make_kn mp dir (label_of_id id) in
Nametab.push_tactic (Until i) sp kn;
add (kn,t)
- | UpdateTac kn ->
- mactab := Gmap.remove kn !mactab;
- add (kn,t)) defs
+ | UpdateTac kn -> replace (kn,t)) defs
let open_md i((sp,kn),defs) =
let dp,_ = repr_path sp in
@@ -2762,10 +2781,7 @@ let open_md i((sp,kn),defs) =
let sp = Libnames.make_path dp id in
let kn = Names.make_kn mp dir (label_of_id id) in
Nametab.push_tactic (Exactly i) sp kn
- | UpdateTac kn ->
- let (path, id) = decode_kn kn in
- let sp = Libnames.make_path path id in
- Nametab.push_tactic (Exactly i) sp kn) defs
+ | UpdateTac kn -> ()) defs
let cache_md x = load_md 1 x
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index add57cb5..b66bdb85 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacinterp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: tacinterp.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
(*i*)
open Dyn
@@ -44,6 +44,9 @@ and interp_sign =
debug : debug_info;
trace : ltac_trace }
+val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env ->
+ Pretyping.var_map * Pretyping.unbound_ltac_var_map
+
(* Transforms an id into a constr if possible *)
val constr_of_id : Environ.env -> identifier -> constr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28e987fa..3db6bcef 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacticals.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
+(* $Id: tacticals.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
open Pp
open Util
@@ -26,7 +26,6 @@ open Clenvtac
open Rawterm
open Pattern
open Matching
-open Evar_refiner
open Genarg
open Tacexpr
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c567034..0a8b5d01 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -155,19 +155,37 @@ let order_hyps = Tacmach.order_hyps
(* Renaming hypotheses *)
let rename_hyp = Tacmach.rename_hyp
+(**************************************************************)
+(* Fresh names *)
+(**************************************************************)
+
+let fresh_id_avoid avoid id =
+ next_global_ident_away true id avoid
+
+let fresh_id avoid id gl =
+ fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
+
+(**************************************************************)
+(* Fixpoints and CoFixpoints *)
+(**************************************************************)
+
(* Refine as a fixpoint *)
let mutual_fix = Tacmach.mutual_fix
-let fix ido n = match ido with
- | None -> mutual_fix (Pfedit.get_current_proof_name ()) n []
- | Some id -> mutual_fix id n []
+let fix ido n gl = match ido with
+ | None ->
+ mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
+ | Some id ->
+ mutual_fix id n [] gl
(* Refine as a cofixpoint *)
let mutual_cofix = Tacmach.mutual_cofix
-let cofix = function
- | None -> mutual_cofix (Pfedit.get_current_proof_name ()) []
- | Some id -> mutual_cofix id []
+let cofix ido gl = match ido with
+ | None ->
+ mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
+ | Some id ->
+ mutual_cofix id [] gl
(**************************************************************)
(* Reduction and conversion tactics *)
@@ -286,12 +304,6 @@ let unfold_constr = function
(* Introduction tactics *)
(*******************************************)
-let fresh_id_avoid avoid id =
- next_global_ident_away true id avoid
-
-let fresh_id avoid id gl =
- fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
-
let id_of_name_with_default id = function
| Anonymous -> id
| Name id -> id
@@ -565,9 +577,14 @@ let error_uninstantiated_metas t clenv =
let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
-let clenv_refine_in with_evars id clenv gl =
+let clenv_refine_in with_evars ?(with_classes=true) id clenv gl =
let clenv = clenv_pose_dependent_evars with_evars clenv in
- let new_hyp_typ = clenv_type clenv in
+ let clenv =
+ if with_classes then
+ { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd }
+ else clenv
+ in
+ let new_hyp_typ = clenv_type clenv in
if not with_evars & occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
@@ -1098,9 +1115,6 @@ let forward_general_multi_rewrite =
let register_general_multi_rewrite f =
forward_general_multi_rewrite := f
-let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
-let case_last = tclLAST_HYP simplest_case
-
let error_unexpected_extra_pattern loc nb pat =
let s1,s2,s3 = match pat with
| IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1111,8 +1125,8 @@ let error_unexpected_extra_pattern loc nb pat =
str (if nb = 1 then "was" else "were") ++
strbrk " expected in the branch).")
-let intro_or_and_pattern loc b ll l' tac =
- tclLAST_HYP (fun c gl ->
+let intro_or_and_pattern loc b ll l' tac id gl =
+ let c = mkVar id in
let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
let nv = mis_constr_nargs ind in
let bracketed = b or not (l'=[]) in
@@ -1126,10 +1140,10 @@ let intro_or_and_pattern loc b ll l' tac =
let ll = fix_empty_or_and_pattern (Array.length nv) ll in
check_or_and_pattern_size loc ll (Array.length nv);
tclTHENLASTn
- (tclTHEN case_last clear_last)
+ (tclTHEN (simplest_case c) (clear [id]))
(array_map2 (fun n l -> tac ((adjust_names_length n n l)@l'))
nv (Array.of_list ll))
- gl)
+ gl
let rewrite_hyp l2r id gl =
let rew_on l2r =
@@ -1194,8 +1208,9 @@ let rec intros_patterns b avoid thin destopt = function
| (loc, IntroOrAndPattern ll) :: l' ->
tclTHEN
introf
- (intro_or_and_pattern loc b ll l'
- (intros_patterns b avoid thin destopt))
+ (onLastHyp
+ (intro_or_and_pattern loc b ll l'
+ (intros_patterns b avoid thin destopt)))
| (loc, IntroRewrite l2r) :: l ->
tclTHEN
(intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
@@ -1229,8 +1244,10 @@ let prepare_intros s ipat gl = match ipat with
| IntroRewrite l2r ->
let id = make_id s gl in
id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
- | IntroOrAndPattern ll -> make_id s gl,
- intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+ | IntroOrAndPattern ll -> make_id s gl,
+ onLastHyp
+ (intro_or_and_pattern loc true ll []
+ (intros_patterns true [] [] no_move))
let ipat_of_name = function
| Anonymous -> None
@@ -1261,6 +1278,7 @@ let as_tac id ipat = match ipat with
!forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
| Some (loc,IntroOrAndPattern ll) ->
intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
+ id
| Some (loc,
(IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
@@ -2167,7 +2185,7 @@ let dependent_pattern c gl =
let conclvar = subst_term_occ all_occurrences c ty in
mkNamedLambda id cty conclvar
in
- let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in
+ let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in
let concllda = List.fold_left mklambda (pf_concl gl) subst in
let conclapp = applistc concllda (List.rev_map pi1 subst) in
convert_concl_no_check conclapp DEFAULTcast gl
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index bd7fd796..fb2725c9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -1,5 +1,5 @@
-Require Import Setoid.
+Require Import Setoid Program.
Axiom t : Set.
Axiom In : nat -> t -> Prop.
diff --git a/test-suite/bugs/closed/shouldsucceed/2089.v b/test-suite/bugs/closed/shouldsucceed/2089.v
new file mode 100644
index 00000000..aebccc94
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2089.v
@@ -0,0 +1,17 @@
+Inductive even (x: nat): nat -> Prop :=
+ | even_base: even x O
+ | even_succ: forall n, odd x n -> even x (S n)
+
+with odd (x: nat): nat -> Prop :=
+ | odd_succ: forall n, even x n -> odd x (S n).
+
+Scheme even_ind2 := Minimality for even Sort Prop
+ with odd_ind2 := Minimality for odd Sort Prop.
+
+Combined Scheme even_odd_ind from even_ind2, odd_ind2.
+
+Check (even_odd_ind :forall (x : nat) (P P0 : nat -> Prop),
+ P 0 ->
+ (forall n : nat, odd x n -> P0 n -> P (S n)) ->
+ (forall n : nat, even x n -> P n -> P0 (S n)) ->
+ (forall n : nat, even x n -> P n) /\ (forall n : nat, odd x n -> P0 n)).
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 488b057f..46dd0cb6 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,5 +1,4 @@
Require Import Coq.Program.Program.
-Set Manual Implicit Arguments.
Variable A : Set.
@@ -105,7 +104,7 @@ Save.
(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
-Unset Manual Implicit Arguments.
+Set Implicit Arguments.
Inductive Ty :=
| Nat : Ty
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 157217ae..15cabf81 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -12,9 +12,7 @@
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
-(* $Id: EquivDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** Export notations. *)
@@ -144,9 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
| _, _ => in_right
end }.
- Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+ Solve Obligations using unfold equiv, complement in *; program_simpl;
+ intuition (discriminate || eauto).
- Next Obligation.
- Proof. clear aux. red in H0. subst.
- destruct y; intuition (discriminate || eauto).
- Defined.
+ Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+
+ Solve Obligations using unfold equiv, complement in *; program_simpl;
+ intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5e5895ab..7068bc6b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -12,15 +12,15 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: Equivalence.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
-Require Export Coq.Program.Basics.
+Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Classes.Init.
Require Import Relation_Definitions.
-Require Import Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 5df7a4ed..762cc5c1 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,12 +13,7 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: Init.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
-
-Tactic Notation "clapply" ident(c) :=
- eapply @c ; typeclasses eauto.
+(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** Hints for the proof search: these combinators should be considered rigid. *)
@@ -29,12 +24,12 @@ Typeclasses Opaque id const flip compose arrow impl iff.
(** The unconvertible typeclass, to test that two objects of the same type are
actually different. *)
-Class Unconvertible (A : Type) (a b : A).
+Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
Ltac unconvertible :=
match goal with
| |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
- | |- _ => eapply Build_Unconvertible
+ | |- _ => exact tt
end.
Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. \ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 86097a56..2b653e27 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,9 +12,7 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: Morphisms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-Set Manual Implicit Arguments.
+(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
@@ -55,18 +52,24 @@ Definition respectful {A B : Type}
(** Notations reminiscent of the old syntax for declaring morphisms. *)
Delimit Scope signature_scope with signature.
+
Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+Module MorphismNotations.
-Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+ Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
+
+ Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
+
+ Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+ (right associativity, at level 55) : signature_scope.
-Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+End MorphismNotations.
-Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+Export MorphismNotations.
Open Local Scope signature_scope.
@@ -118,7 +121,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
(** And of course it is reflexive. *)
-Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Instance morphisms_subrelation_refl : ! subrelation A R R.
Proof. simpl_relation. Qed.
(** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -151,10 +154,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
-Instance iff_impl_subrelation : subrelation iff impl.
+Instance iff_impl_subrelation : subrelation iff impl | 2.
Proof. firstorder. Qed.
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
Proof. firstorder. Qed.
Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
@@ -372,25 +375,6 @@ Ltac partial_application_tactic :=
end
end.
-Section PartialAppTest.
- Instance and_ar : Params and 0.
-
- Goal Morphism (iff) (and True True).
- partial_application_tactic.
- Admitted.
-
- Goal Morphism (iff) (or True True).
- partial_application_tactic.
- partial_application_tactic.
- Admitted.
-
- Goal Morphism (iff ==> iff) (iff True).
- partial_application_tactic.
- (*partial_application_tactic. *)
- Admitted.
-
-End PartialAppTest.
-
Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 24b8d636..4654e654 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -12,6 +12,7 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
+Require Import Relation_Definitions.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Program.Program.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f95894be..e1de9ee9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -13,12 +13,12 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Relations.Relation_Definitions.
(** We allow to unfold the [relation] definition while doing morphism search. *)
@@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
We give an equivalent definition, up-to an equivalence relation
on the carrier. *)
-Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
(** The equivalence proof is sufficient for proving that [R] must be a morphism
@@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
Proof with auto.
- reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe.
+ reduce_goal.
+ pose proof partial_order_equivalence as poe. do 3 red in poe.
apply <- poe. firstorder.
Qed.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 305168ec..03bb9a80 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -12,7 +12,7 @@
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
-(* $Id: SetoidAxioms.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
Require Import Coq.Program.Program.
@@ -22,7 +22,7 @@ Unset Strict Implicit.
Require Export Coq.Classes.SetoidClass.
(* Application of the extensionality axiom to turn a goal on
- Leibinz equality to a setoid equivalence (use with care!). *)
+ Leibniz equality to a setoid equivalence (use with care!). *)
Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 47f92ada..d3da7d5a 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -12,14 +12,14 @@
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
91405 Orsay, France *)
-(* $Id: SetoidClass.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *)
Set Implicit Arguments.
Unset Strict Implicit.
Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
Require Export Coq.Classes.RelationClasses.
Require Export Coq.Classes.Morphisms.
Require Import Coq.Classes.Functions.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index caacc9ec..36f05e31 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,13 +13,13 @@
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
-(* $Id: SetoidTactics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *)
-Require Export Coq.Classes.RelationClasses.
-Require Export Coq.Classes.Morphisms.
-Require Export Coq.Classes.Morphisms_Prop.
-Require Export Coq.Classes.Equivalence.
-Require Export Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
+Require Import Coq.Classes.Equivalence Coq.Program.Basics.
+
+Export MorphismNotations.
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index df12166e..d91eb87a 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 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FMapFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** * Finite maps library *)
@@ -15,7 +15,7 @@
different styles: equivalence and boolean equalities.
*)
-Require Import Bool DecidableType DecidableTypeEx OrderedType.
+Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.
Require Export FMapInterface.
Set Implicit Arguments.
Unset Strict Implicit.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 1e15d3a1..674caaac 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: FSetFacts.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id: FSetFacts.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** * Finite sets library *)
@@ -17,7 +17,7 @@
*)
Require Import DecidableTypeEx.
-Require Export FSetInterface.
+Require Export FSetInterface.
Set Implicit Arguments.
Unset Strict Implicit.
@@ -424,14 +424,14 @@ Add Relation t Subset
transitivity proved by Subset_trans
as SubsetSetoid.
-Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
+Instance In_s_m : Morphisms.Morphism (E.eq ==> Subset ++> Basics.impl) In | 1.
Proof.
simpl_relation. eauto with set.
Qed.
-Add Morphism Empty with signature Subset --> impl as Empty_s_m.
+Add Morphism Empty with signature Subset --> Basics.impl as Empty_s_m.
Proof.
-unfold Subset, Empty, impl; firstorder.
+unfold Subset, Empty, Basics.impl; firstorder.
Qed.
Add Morphism add with signature E.eq ==> Subset ++> Subset as add_s_m.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 3753b97b..ff70c9fb 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
(** This module proves the constructive description schema, which
infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -14,8 +14,8 @@ predicate from the regular existence (i.e., [Prop]-existence). One
requires that the underlying set is countable and that the predicate
is decidable. *)
-(** Coq does not allow case analysis on sort [Set] when the goal is in
-[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+(** Coq does not allow case analysis on sort [Prop] when the goal is in
+[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
show [{n : nat | P n}]. However, one can perform a recursion on an
inductive predicate in sort [Prop] so that the returning type of the
recursion is in [Set]. This trick is described in Coq'Art book, Sect.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index 4445b0e1..0dc82907 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -11,8 +11,6 @@
(** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
-Set Manual Implicit Arguments.
-
(** The converse of functional extensionality. *)
Lemma equal_f : forall {A B : Type} {f g : A -> B},
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 99d54755..9681d543 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Equality.v 11709 2008-12-20 11:42:15Z msozeau $ i*)
+(*i $Id: Equality.v 12073 2009-04-08 21:04:42Z msozeau $ i*)
(** Tactics related to (dependent) equality and proof irrelevance. *)
@@ -479,8 +479,12 @@ Ltac intro_prototypes :=
| _ => idtac
end.
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
-Ltac do_ind p := induction p || elim_ind p.
+Ltac introduce p :=
+ first [ match p with _ => idtac end (* Already there *)
+ | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 12bdf3a7..2083e530 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Wf.v 11709 2008-12-20 11:42:15Z msozeau $ *)
+(* $Id: Wf.v 12187 2009-06-13 19:36:59Z msozeau $ *)
(** Reformulation of the Wf module using subsets where possible, providing
the support for [Program]'s treatment of well-founded definitions. *)
@@ -165,7 +165,7 @@ Section Measure_well_founded.
(* Measure relations are well-founded if the underlying relation is well-founded. *)
- Variables T M: Set.
+ Variables T M: Type.
Variable R: M -> M -> Prop.
Hypothesis wf: well_founded R.
Variable m: T -> M.
@@ -191,7 +191,7 @@ End Measure_well_founded.
Section Fix_measure_rects.
- Variable A: Set.
+ Variable A: Type.
Variable m: A -> nat.
Variable P: A -> Type.
Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
@@ -287,7 +287,7 @@ Section Fix_measure_rects.
End Fix_measure_rects.
-(** Tactic to fold a definitions based on [Fix_measure_sub]. *)
+(** Tactic to fold a definition based on [Fix_measure_sub]. *)
Ltac fold_sub f :=
match goal with
@@ -312,8 +312,8 @@ Module WfExtensionality.
(** For a function defined with Program using a well-founded order. *)
Program Lemma fix_sub_eq_ext :
- forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
- (P : A -> Set)
+ forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+ (P : A -> Type)
(F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
forall x : A,
Fix_sub A R Rwf P F_sub x =
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index e7fe82b2..a187a7c6 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -6,10 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Setoid.v 11720 2008-12-28 07:12:15Z letouzey $: i*)
+(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*)
Require Export Coq.Classes.SetoidTactics.
+Export Morphisms.MorphismNotations.
+
(** For backward compatibility *)
Definition Setoid_Theory := @Equivalence.
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 98457261..eb3a19fa 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *)
+(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -212,7 +212,7 @@ let clean sds sps =
print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
$(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
if !some_mlfile then
- print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
+ print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n";
if Coq_config.has_natdynlink && !some_mlfile then
print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n";
print "\t- rm -rf html\n";
@@ -243,14 +243,14 @@ let footer_includes () =
let implicit () =
let ml_rules () =
print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
- print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
- print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n";
- print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
+ print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+ print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+ print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
- print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
+ print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
print "%.ml.d: %.ml\n";
- print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
+ print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n"
and v_rule () =
print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -283,8 +283,8 @@ let variables defs =
print "COQDOC:=$(COQBIN)coqdoc\n";
print "COQMKTOP:=$(COQBIN)coqmktop\n";
(* Caml executables and relative variables *)
- printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
- printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
+ printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc;
+ printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt;
printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
print "GRAMMARS:=grammar.cma\n";
@@ -315,7 +315,7 @@ let include_dirs (inc_i,inc_r) =
let str_i' = parse_includes inc_i' in
let str_r = parse_rec_includes inc_r in
section "Libraries definitions.";
- print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n";
+ print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n";
print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
-I $(COQLIB)/library -I $(COQLIB)/parsing \\
-I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5bcbed64..b3f0739d 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -54,9 +54,10 @@ let toc = ref false
let page_title = ref ""
let title = ref ""
let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
+let coqlib = ref Coq_config.wwwstdlib
let coqlib_path = ref Coq_config.coqlib
let raw_comments = ref false
+let parse_comments = ref false
let interpolate = ref false
let charset = ref "iso-8859-1"
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index a9a99706..762be5af 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -57,6 +57,11 @@ body { padding: 0px 0px;
display: inline;
font-family: monospace }
+.comment {
+ display: inline;
+ font-family: monospace;
+ color: red; }
+
.code {
display: block;
font-family: monospace }
@@ -80,18 +85,46 @@ body { padding: 0px 0px;
color: rgb(40%,0%,40%);
}
+.id[type="variable"] {
+ color: rgb(40%,0%,40%);
+}
+
.id[type="definition"] {
color: rgb(0%,40%,0%);
}
+.id[type="abbreviation"] {
+ color: rgb(0%,40%,0%);
+}
+
.id[type="lemma"] {
color: rgb(0%,40%,0%);
}
+.id[type="instance"] {
+ color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] {
+ color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] {
+ color: rgb(0%,40%,0%);
+}
+
.id[type="inductive"] {
color: rgb(0%,0%,80%);
}
+.id[type="record"] {
+ color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] {
+ color: rgb(0%,0%,80%);
+}
+
.id[type="keyword"] {
color : #cf1d1d;
/* color: black; */
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index ef4f4119..fca9a1d7 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -70,6 +70,9 @@
% !!! CAUTION: This environment may have empty contents
\newenvironment{coqdoccode}{}{}
+% Environment for comments
+\newenvironment{coqdoccomment}{\tt(*}{*)}
+
% newline and indentation
%BEGIN LATEX
% Base indentation length
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2e97618b..2ee9ac96 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*)
+(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
* - handling of absolute filenames (function coq_module)
@@ -56,7 +56,7 @@ let usage () =
prerr_endline " --verbose verbose mode";
prerr_endline " --no-externals no links to Coq standard library";
prerr_endline " --coqlib <url> set URL for Coq standard library";
- prerr_endline " (default is http://coq.inria.fr/library/)";
+ prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")");
prerr_endline " --boot run in boot mode";
prerr_endline " --coqlib_path <dir> set the path where Coq files are installed";
prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir";
@@ -65,6 +65,7 @@ let usage () =
prerr_endline " --charset <string> set HTML charset";
prerr_endline " --inputenc <string> set LaTeX input encoding";
prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module";
+ prerr_endline " --parse-comments parse regular comments";
prerr_endline "";
exit 1
@@ -273,6 +274,8 @@ let parse () =
usage ()
| ("-raw-comments" | "--raw-comments") :: rem ->
Cdglobals.raw_comments := true; parse_rec rem
+ | ("-parse-comments" | "--parse-comments") :: rem ->
+ Cdglobals.parse_comments := true; parse_rec rem
| ("-interpolate" | "--interpolate") :: rem ->
Cdglobals.interpolate := true; parse_rec rem
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c146150c..1ad8b14f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
open Cdglobals
open Index
@@ -292,13 +292,13 @@ module Latex = struct
let ident s l =
if !in_title then (
- printf "\\texorpdfstring{";
+ printf "\\texorpdfstring{\\protect";
with_latex_printing (fun s -> ident s l) s;
printf "}{"; raw_ident s; printf "}")
else
with_latex_printing (fun s -> ident s l) s
- let symbol = with_latex_printing raw_ident
+ let symbol s = with_latex_printing raw_ident s
let rec reach_item_level n =
if !item_level < n then begin
@@ -320,6 +320,12 @@ module Latex = struct
let end_doc () = in_doc := false; stop_item ()
+ let comment c = char c
+
+ let start_comment () = printf "\\begin{coqdoccomment}\n"
+
+ let end_comment () = printf "\\end{coqdoccomment}\n"
+
let start_coq () = printf "\\begin{coqdoccode}\n"
let end_coq () = printf "\\end{coqdoccode}\n"
@@ -389,8 +395,6 @@ module Html = struct
printf "<div id=\"main\">\n\n"
end
- let self = "http://coq.inria.fr"
-
let trailer () =
if !index && !current_module <> "Index" then
printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
@@ -406,7 +410,7 @@ module Html = struct
else
begin
printf "<hr/>This page has been generated by ";
- printf "<a href=\"%s\">coqdoc</a>\n" self;
+ printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
printf "</div>\n\n</div>\n\n</body>\n</html>"
end
@@ -456,14 +460,15 @@ module Html = struct
let ident_ref m fid typ s =
match find_module m with
| Local ->
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
printf "<span class=\"id\" type=\"%s\">" typ;
- printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
- printf "</a></span>"
+ raw_ident s;
+ printf "</span></a>"
| Coqlib when !externals ->
let m = Filename.concat !coqlib m in
- printf "<span class=\"id\" type=\"%s\">" typ;
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
- raw_ident s; printf "</a></span>"
+ printf "<span class=\"id\" type=\"%s\">" typ;
+ raw_ident s; printf "</span></a>"
| Coqlib | Unknown ->
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
@@ -477,8 +482,9 @@ module Html = struct
try
(match Index.find !current_module loc with
| Def (fullid,ty) ->
+ printf "<a name=\"%s\">" fullid;
printf "<span class=\"id\" type=\"%s\">" (type_name ty);
- printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
+ raw_ident s; printf "</span></a>"
| Mod (m,s') when s = s' ->
module_ref m s
| Ref (m,fullid,ty) ->
@@ -500,9 +506,11 @@ module Html = struct
with Not_found ->
f tok
- let ident s l = with_html_printing (fun s -> ident s l) s
+ let ident s l =
+ with_html_printing (fun s -> ident s l) s
- let symbol = with_html_printing raw_ident
+ let symbol s =
+ with_html_printing raw_ident s
let rec reach_item_level n =
if !item_level < n then begin
@@ -532,6 +540,10 @@ module Html = struct
stop_item ();
if not !raw_comments then printf "\n</div>\n"
+ let start_comment () = printf "<span class=\"comment\">(*"
+
+ let end_comment () = printf "*)</span>"
+
let start_code () = end_doc (); start_coq ()
let end_code () = end_coq (); start_doc ()
@@ -540,7 +552,11 @@ module Html = struct
let end_inline_coq () = printf "</span>"
- let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+ let paragraph () =
+ let i = !item_level in
+ stop_item ();
+ if i > 0 then printf "\n"
+ else printf "\n<br/> <br/>\n"
let section lev f =
let lab = new_label () in
@@ -770,6 +786,9 @@ module TeXmacs = struct
let end_coq () = ()
+ let start_comment () = ()
+ let end_comment () = ()
+
let start_code () = in_doc := true; printf "<\\code>\n"
let end_code () = in_doc := false; printf "\n</code>"
@@ -849,7 +868,7 @@ module Raw = struct
let ident s loc = raw_ident s
- let symbol = raw_ident
+ let symbol s = raw_ident s
let item n = printf "- "
@@ -858,6 +877,9 @@ module Raw = struct
let start_doc () = printf "(** "
let end_doc () = printf " *)\n"
+ let start_comment () = ()
+ let end_comment () = ()
+
let start_coq () = ()
let end_coq () = ()
@@ -911,6 +933,9 @@ let start_module =
let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc
+let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment
+let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment
+
let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq
let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 3da80335..75c7ccf8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
open Cdglobals
open Index
@@ -28,6 +28,9 @@ val start_module : unit -> unit
val start_doc : unit -> unit
val end_doc : unit -> unit
+val start_comment : unit -> unit
+val end_comment : unit -> unit
+
val start_coq : unit -> unit
val end_coq : unit -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 3ae5cbed..c4a1a76f 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*)
+(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*s Utility functions for the scanners *)
@@ -57,7 +57,7 @@
let formatted = ref false
let brackets = ref 0
let comment_level = ref 0
- let in_proof = ref false
+ let in_proof = ref None
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
@@ -162,6 +162,8 @@
else
String.sub s 1 (String.length s - 3)
+ let symbol lexbuf s = Output.symbol s
+
}
(*s Regular expressions *)
@@ -217,7 +219,10 @@ let thm_token =
| "Proposition"
| "Property"
| "Goal"
- | "Next" space+ "Obligation"
+
+let prf_token =
+ "Next" space+ "Obligation"
+ | "Proof" (space* "." | space+ "with")
let def_token =
"Definition"
@@ -290,7 +295,7 @@ let commands =
| ("Hypothesis" | "Hypotheses")
| "End"
-let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
let extraction =
"Extraction"
@@ -307,7 +312,6 @@ let prog_kw =
let gallina_kw_to_hide =
"Implicit" space+ "Arguments"
- | "Next" "Obligation"
| "Ltac"
| "Require"
| "Import"
@@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
rule coq_bol = parse
| space* nl+
- { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf }
+ { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
| space* "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
@@ -379,27 +383,29 @@ rule coq_bol = parse
Output.indentation nbsp;
Output.ident s (lexeme_start lexbuf + isp);
let eol = body lexbuf in
- in_proof := true;
+ in_proof := Some eol;
if eol then coq_bol lexbuf else coq lexbuf }
- | space* "Proof" (space* "." | space+ "with")
- { in_proof := true;
+ | space* prf_token
+ { in_proof := Some true;
let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else true
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
+ let s = lexeme lexbuf in
+ if s.[String.length s - 1] = '.' then false
+ else skip_to_dot lexbuf
in if eol then coq_bol lexbuf else coq lexbuf }
| space* end_kw {
let eol =
- if not (!in_proof && !Cdglobals.gallina) then
+ if not (!in_proof <> None && !Cdglobals.gallina) then
begin backtrack lexbuf; body_bol lexbuf end
- else
- skip_to_dot lexbuf
+ else skip_to_dot lexbuf
in
- in_proof := false;
+ in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| space* gallina_kw
{
- in_proof := false;
+ in_proof := None;
let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
let s = String.sub s isp (String.length s - isp) in
@@ -409,7 +415,7 @@ rule coq_bol = parse
if eol then coq_bol lexbuf else coq lexbuf }
| space* prog_kw
{
- in_proof := false;
+ in_proof := None;
let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
@@ -441,6 +447,12 @@ rule coq_bol = parse
coq_bol lexbuf }
| space* "(*"
{ comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
let eol = comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| eof
@@ -458,7 +470,7 @@ rule coq_bol = parse
and coq = parse
| nl
- { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+ { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
| "(**" space_nl
{ Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
@@ -466,12 +478,18 @@ and coq = parse
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
let eol = comment lexbuf in
- if eol then begin Output.line_break(); coq_bol lexbuf end
+ if eol then coq_bol lexbuf
else coq lexbuf
}
| nl+ space* "]]"
- { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
+ { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
| eof
{ () }
| gallina_kw_to_hide
@@ -487,14 +505,29 @@ and coq = parse
let eol=body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
+ | prf_token
+ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
+ let s = lexeme lexbuf in
+ let eol =
+ if s.[String.length s - 1] = '.' then false
+ else skip_to_dot lexbuf
+ in
+ eol
+ in if eol then coq_bol lexbuf else coq lexbuf }
| end_kw {
let eol =
- if not (!in_proof && !Cdglobals.gallina) then
+ if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
- else
- skip_to_dot lexbuf
+ else
+ let eol = skip_to_dot lexbuf in
+ if !in_proof <> Some true && eol then
+ Output.line_break ();
+ eol
in
- in_proof := false;
+ in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| gallina_kw
{ let s = lexeme lexbuf in
@@ -513,8 +546,7 @@ and coq = parse
if not !Cdglobals.gallina then
begin backtrack lexbuf; body lexbuf end
else
- let eol = skip_to_dot lexbuf in
- if eol then Output.line_break (); eol
+ skip_to_dot lexbuf
in
if eol then coq_bol lexbuf else coq lexbuf}
@@ -616,8 +648,7 @@ and escaped_coq = parse
{ () }
| token_brackets
{ let s = lexeme lexbuf in
- Output.symbol s;
- escaped_coq lexbuf }
+ symbol lexbuf s; escaped_coq lexbuf }
| (identifier '.')* identifier
{ Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
| _
@@ -644,15 +675,30 @@ and comments = parse
(*s Skip comments *)
and comment = parse
- | "(*" { incr comment_level; comment lexbuf }
- | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | eof { false }
- | _ { comment lexbuf }
-
+ | "(*" { incr comment_level;
+ if !Cdglobals.parse_comments then Output.start_comment ();
+ comment lexbuf }
+ | "*)" space* nl {
+ if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ());
+ decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+ | "*)" {
+ if !Cdglobals.parse_comments then (Output.end_comment ());
+ decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+ | "[" {
+ if !Cdglobals.parse_comments then (
+ brackets := 1;
+ Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
+ comment lexbuf }
+ | eof { false }
+ | space+ { if !Cdglobals.parse_comments then
+ Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
+ | nl { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+ | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+ comment lexbuf }
+
and skip_to_dot = parse
| '.' space* nl { true }
- | eof | '.' space+ { false}
+ | eof | '.' space+ { false }
| "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }
@@ -664,15 +710,19 @@ and body_bol = parse
and body = parse
| nl {Output.line_break(); body_bol lexbuf}
| nl+ space* "]]"
- { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
+ { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
| eof { false }
- | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }
- | '.' space+ { Output.char '.'; Output.char ' '; false }
+ | '.' space* nl | '.' space* eof
+ { Output.char '.'; Output.line_break();
+ if not !formatted then true else body_bol lexbuf }
+ | '.' space+ { Output.char '.'; Output.char ' ';
+ if not !formatted then false else body lexbuf }
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
| "(*" { comment_level := 1;
+ if !Cdglobals.parse_comments then Output.start_comment ();
let eol = comment lexbuf in
if eol
- then begin Output.line_break(); body_bol lexbuf end
+ then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
else body lexbuf }
| identifier
{ let s = lexeme lexbuf in
@@ -680,7 +730,7 @@ and body = parse
body lexbuf }
| token_no_brackets
{ let s = lexeme lexbuf in
- Output.symbol s; body lexbuf }
+ symbol lexbuf s; body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
body lexbuf }
@@ -695,7 +745,7 @@ and notation = parse
| '"' { Output.char '"'}
| token
{ let s = lexeme lexbuf in
- Output.symbol s; notation lexbuf }
+ symbol lexbuf s; notation lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
notation lexbuf }
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 04945040..1a1640a4 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
+(*i $Id: classes.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Names
@@ -264,6 +264,14 @@ let named_of_rel_context l =
l ([], [])
in ctx
+let push_named_context = List.fold_right push_named
+
+let rec list_filter_map f = function
+ | [] -> []
+ | hd :: tl -> match f hd with
+ | None -> list_filter_map f tl
+ | Some x -> x :: list_filter_map f tl
+
let context ?(hook=fun _ -> ()) l =
let env = Global.env() in
let evars = ref (Evd.create_evar_defs Evd.empty) in
@@ -274,6 +282,14 @@ let context ?(hook=fun _ -> ()) l =
let ctx = try named_of_rel_context fullctx with _ ->
error "Anonymous variables not allowed in contexts."
in
+ let env = push_named_context ctx env in
+ let keeps =
+ List.fold_left (fun acc (id,_,t) ->
+ match class_of_constr t with
+ | None -> acc
+ | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc)
+ [] ctx
+ in
List.iter (function (id,_,t) ->
if Lib.is_modtype () then
let cst = Declare.declare_internal_constant id
@@ -285,10 +301,14 @@ let context ?(hook=fun _ -> ()) l =
hook (ConstRef cst)
| None -> ()
else (
- let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+ let impl = List.exists (fun (x,_) ->
+ match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+ and keep =
+ let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in
+ List.concat l
in
Command.declare_one_assumption false (Local (* global *), Definitional) t
- [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+ [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id);
match class_of_constr t with
| None -> ()
| Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b50c9bbd..05a22829 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: command.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
open Pp
open Util
@@ -546,7 +546,7 @@ let interp_mutual paramsl indl notations finite =
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
- States.with_heavy_rollback (fun () ->
+ States.with_state_protection (fun () ->
(* Temporary declaration of notations and scopes *)
List.iter (declare_interning_data impls) notations;
(* Interpret the constructor types *)
@@ -851,7 +851,7 @@ let interp_recursive fixkind l boxed =
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
- States.with_heavy_rollback (fun () ->
+ States.with_state_protection (fun () ->
List.iter (declare_interning_data impls) notations;
list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
() in
@@ -1012,16 +1012,18 @@ let build_combined_scheme name schemes =
let (ctx, arity) = decompose_prod ty in
let (_, last) = List.hd ctx in
match kind_of_term last with
- | App (ind, args) -> ctx, destInd ind, Array.length args
+ | App (ind, args) ->
+ let ind = destInd ind in
+ let (_,spec) = Inductive.lookup_mind_specif env ind in
+ ctx, ind, spec.mind_nrealargs
| _ -> ctx, destInd last, 0
in
let defs =
List.map (fun x ->
let refe = Ident x in
let qualid = qualid_of_reference refe in
- let cst = try
- Nametab.locate_constant (snd qualid)
- with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
+ let cst = try Nametab.locate_constant (snd qualid)
+ with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
in
let ty = Typeops.type_of_constant env cst in
qualid, cst, ty)
@@ -1087,9 +1089,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
| None ->
(match local with
| Local ->
- let impl=false and keep=false in (* copy values from Vernacentries *)
+ let impl=false in (* copy values from Vernacentries *)
let k = IsAssumption Conjectural in
- let c = SectionLocalAssum (t_i,impl,keep) in
+ let c = SectionLocalAssum (t_i,impl,[]) in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Local,VarRef id,imps)
| Global ->
@@ -1123,9 +1125,9 @@ let look_for_mutual_statements thms =
let n = List.length thms in
let inds = List.map (fun (id,(t,_) as x) ->
let (hyps,ccl) = Sign.decompose_prod_assum t in
- let whnf_hyp_hds = map_rel_context_with_binders
- (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
- hyps in
+ let whnf_hyp_hds = fold_map_rel_context
+ (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+ (Global.env()) hyps in
let ind_hyps =
List.flatten (list_map_i (fun i (_,b,t) ->
match kind_of_term t with
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b42fafd0..36399029 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: command.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: command.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
(*i*)
open Util
@@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
Impargs.manual_explicitation list ->
- bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit
+ bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located -> unit
val set_declare_assumption_hook : (types -> unit) -> unit
val declare_assumption : identifier located list ->
coercion_flag -> assumption_kind -> local_binder list -> constr_expr ->
- bool -> bool -> bool -> unit
+ bool -> identifier list -> bool -> unit
val declare_interning_data : 'a * Constrintern.implicits_env ->
string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f733a3d5..0cda7c71 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *)
open Pp
open Util
@@ -814,8 +814,8 @@ let explain_ltac_call_trace (last,trace,loc) =
(if unboundvars <> [] or vars <> [] then
strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) ->
pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
- (List.rev vars @ unboundvars)
- else mt()) ++ str ")" in
+ (List.rev vars @ unboundvars) ++ str ")"
+ else mt()) in
if calls <> [] then
let kind_of_last_call = match list_last calls with
| Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 4a2ef7db..4c0e34cd 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: record.ml 12080 2009-04-11 16:56:20Z herbelin $ *)
open Pp
open Util
@@ -366,7 +366,7 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
(* Now, younger decl in params and fields is on top *)
let sc = Option.map mkSort s in
let implpars, params, implfs, fields =
- States.with_heavy_rollback (fun () ->
+ States.with_state_protection (fun () ->
typecheck_params_and_fields idstruc sc ps notations fs) ()
in
match kind with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c95c89d3..6a0acb52 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -373,7 +373,7 @@ let vernac_assumption kind l nl=
List.iter (fun lid ->
if global then Dumpglob.dump_definition lid false "ax"
else Dumpglob.dump_definition lid true "var") idl;
- declare_assumption idl is_coe kind [] c false false nl) l
+ declare_assumption idl is_coe kind [] c false [] nl) l
let vernac_record k finite struc binders sort nameopt cfs =
let const = match nameopt with
@@ -810,14 +810,6 @@ let _ =
let _ =
declare_bool_option
{ optsync = true;
- optname = "manual implicit arguments";
- optkey = (TertiaryTable ("Manual","Implicit","Arguments"));
- optread = Impargs.is_manual_implicit_args;
- optwrite = Impargs.make_manual_implicit_args }
-
-let _ =
- declare_bool_option
- { optsync = true;
optname = "strict implicit arguments";
optkey = (SecondaryTable ("Strict","Implicit"));
optread = Impargs.is_strict_implicit_args;
@@ -1110,9 +1102,10 @@ let vernac_print = function
| PrintAbout qid -> msgnl (print_about qid)
| PrintImplicit qid -> msg (print_impargs qid)
(*spiwack: prints all the axioms and section variables used by a term *)
- | PrintAssumptions r ->
+ | PrintAssumptions (o,r) ->
let cstr = constr_of_global (global_with_alias r) in
- let nassumptions = Environ.assumptions cstr (Global.env ()) in
+ let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
+ ~add_opaque:o cstr (Global.env ()) in
msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
let global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 3e9dfb25..4da16ea7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacexpr.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
+(*i $Id: vernacexpr.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
open Util
open Names
@@ -65,7 +65,7 @@ type printable =
| PrintVisibility of string option
| PrintAbout of reference
| PrintImplicit of reference
- | PrintAssumptions of reference
+ | PrintAssumptions of bool * reference
type search_about_item =
| SearchSubPattern of constr_pattern_expr