diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
| commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
| tree | d4c4a873eb055c728666f367469fa26c3417793a | |
| parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) | |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
121 files changed, 1125 insertions, 879 deletions
@@ -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 ========================= @@ -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) @@ -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) *************************************************************************** @@ -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 @@ -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>: @@ -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; @@ -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 |