diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
131 files changed, 1170 insertions, 1170 deletions
@@ -30,7 +30,7 @@ interp/topconstr.cmi: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \ lib/pp.cmi kernel/names.cmi kernel/mod_subst.cmi library/libnames.cmi \ pretyping/evd.cmi lib/dyn.cmi lib/bigint.cmi kernel/cbytecodes.cmi: kernel/term.cmi kernel/names.cmi -kernel/cbytegen.cmi: kernel/term.cmi kernel/names.cmi kernel/environ.cmi \ +kernel/cbytegen.cmi: kernel/term.cmi kernel/pre_env.cmi kernel/names.cmi \ kernel/declarations.cmi kernel/cemitcodes.cmi kernel/cbytecodes.cmi kernel/cemitcodes.cmi: kernel/names.cmi kernel/mod_subst.cmi \ kernel/cbytecodes.cmi @@ -39,27 +39,30 @@ kernel/closure.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi \ kernel/conv_oracle.cmi: kernel/names.cmi kernel/cooking.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi kernel/environ.cmi kernel/declarations.cmi -kernel/csymtable.cmi: kernel/term.cmi kernel/names.cmi kernel/environ.cmi +kernel/csymtable.cmi: kernel/term.cmi kernel/pre_env.cmi kernel/names.cmi kernel/declarations.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ lib/rtree.cmi kernel/names.cmi kernel/mod_subst.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi kernel/entries.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi kernel/environ.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ - kernel/names.cmi kernel/declarations.cmi + kernel/pre_env.cmi kernel/names.cmi kernel/declarations.cmi \ + kernel/cemitcodes.cmi kernel/esubst.cmi: lib/util.cmi kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \ kernel/names.cmi kernel/environ.cmi kernel/entries.cmi \ kernel/declarations.cmi kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi kernel/declarations.cmi -kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi -kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ - kernel/declarations.cmi kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \ kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \ kernel/declarations.cmi +kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi +kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \ + kernel/declarations.cmi kernel/names.cmi: lib/predicate.cmi lib/pp.cmi +kernel/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ + kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi kernel/reduction.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/environ.cmi kernel/safe_typing.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \ @@ -82,13 +85,10 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi lib/bigint.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi lib/compat.cmo library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \ library/nametab.cmi kernel/names.cmi library/libnames.cmi \ - kernel/indtypes.cmi kernel/entries.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo + kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \ + kernel/declarations.cmi library/decl_kinds.cmo library/declaremods.cmi: lib/util.cmi kernel/safe_typing.cmi lib/pp.cmi \ kernel/names.cmi library/libobject.cmi library/libnames.cmi \ library/lib.cmi kernel/environ.cmi kernel/entries.cmi @@ -115,6 +115,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \ library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \ library/libnames.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi lib/compat.cmo parsing/ast.cmi: lib/util.cmi interp/topconstr.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi library/libnames.cmi \ interp/genarg.cmi lib/dyn.cmi parsing/coqast.cmi @@ -350,11 +353,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \ toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \ library/libobject.cmi toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi -toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \ kernel/environ.cmi translate/ppconstrnew.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ @@ -377,9 +380,9 @@ contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \ kernel/term.cmi kernel/names.cmi -contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi +contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \ @@ -399,8 +402,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \ kernel/names.cmi contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi contrib/correctness/pwp.cmi: kernel/term.cmi -contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi +contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi @@ -524,6 +527,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi +ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ + lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ + ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ + ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi +ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ + lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ + ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ + ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \ @@ -548,14 +559,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi -ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ - lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \ - ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \ - ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi -ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ - lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \ - ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \ - ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -674,22 +677,22 @@ interp/topconstr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ interp/topconstr.cmi kernel/cbytecodes.cmo: kernel/term.cmi kernel/names.cmi kernel/cbytecodes.cmi kernel/cbytecodes.cmx: kernel/term.cmx kernel/names.cmx kernel/cbytecodes.cmi -kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \ - kernel/environ.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ +kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/pre_env.cmi \ + kernel/names.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ kernel/cbytecodes.cmi kernel/cbytegen.cmi -kernel/cbytegen.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \ - kernel/environ.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ +kernel/cbytegen.cmx: lib/util.cmx kernel/term.cmx kernel/pre_env.cmx \ + kernel/names.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ kernel/cbytecodes.cmx kernel/cbytegen.cmi kernel/cemitcodes.cmo: kernel/term.cmi kernel/names.cmi kernel/mod_subst.cmi \ kernel/copcodes.cmo kernel/cbytecodes.cmi kernel/cemitcodes.cmi kernel/cemitcodes.cmx: kernel/term.cmx kernel/names.cmx kernel/mod_subst.cmx \ kernel/copcodes.cmx kernel/cbytecodes.cmx kernel/cemitcodes.cmi -kernel/closure.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi kernel/names.cmi \ - kernel/esubst.cmi kernel/environ.cmi kernel/declarations.cmi \ - kernel/closure.cmi -kernel/closure.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx kernel/names.cmx \ - kernel/esubst.cmx kernel/environ.cmx kernel/declarations.cmx \ - kernel/closure.cmi +kernel/closure.cmo: lib/util.cmi kernel/term.cmi kernel/sign.cmi lib/pp.cmi \ + kernel/names.cmi kernel/esubst.cmi kernel/environ.cmi \ + kernel/declarations.cmi kernel/closure.cmi +kernel/closure.cmx: lib/util.cmx kernel/term.cmx kernel/sign.cmx lib/pp.cmx \ + kernel/names.cmx kernel/esubst.cmx kernel/environ.cmx \ + kernel/declarations.cmx kernel/closure.cmi kernel/conv_oracle.cmo: kernel/names.cmi kernel/conv_oracle.cmi kernel/conv_oracle.cmx: kernel/names.cmx kernel/conv_oracle.cmi kernel/cooking.cmo: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ @@ -698,11 +701,11 @@ kernel/cooking.cmo: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ kernel/cooking.cmx: lib/util.cmx kernel/term.cmx kernel/sign.cmx \ kernel/reduction.cmx lib/pp.cmx kernel/names.cmx kernel/environ.cmx \ kernel/declarations.cmx kernel/cemitcodes.cmx kernel/cooking.cmi -kernel/csymtable.cmo: kernel/vm.cmi kernel/term.cmi kernel/names.cmi \ - kernel/environ.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ +kernel/csymtable.cmo: kernel/vm.cmi kernel/term.cmi kernel/pre_env.cmi \ + kernel/names.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ kernel/cbytegen.cmi kernel/cbytecodes.cmi kernel/csymtable.cmi -kernel/csymtable.cmx: kernel/vm.cmx kernel/term.cmx kernel/names.cmx \ - kernel/environ.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ +kernel/csymtable.cmx: kernel/vm.cmx kernel/term.cmx kernel/pre_env.cmx \ + kernel/names.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ kernel/cbytegen.cmx kernel/cbytecodes.cmx kernel/csymtable.cmi kernel/declarations.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/sign.cmi lib/rtree.cmi kernel/names.cmi kernel/mod_subst.cmi \ @@ -715,10 +718,12 @@ kernel/entries.cmo: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ kernel/entries.cmx: kernel/univ.cmx kernel/term.cmx kernel/sign.cmx \ kernel/names.cmx kernel/entries.cmi kernel/environ.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ - kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi \ + kernel/sign.cmi kernel/pre_env.cmi kernel/names.cmi \ + kernel/declarations.cmi kernel/csymtable.cmi kernel/cbytegen.cmi \ kernel/environ.cmi kernel/environ.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \ - kernel/sign.cmx kernel/names.cmx kernel/declarations.cmx \ + kernel/sign.cmx kernel/pre_env.cmx kernel/names.cmx \ + kernel/declarations.cmx kernel/csymtable.cmx kernel/cbytegen.cmx \ kernel/environ.cmi kernel/esubst.cmo: lib/util.cmi kernel/esubst.cmi kernel/esubst.cmx: lib/util.cmx kernel/esubst.cmi @@ -736,6 +741,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \ kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \ kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \ kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi +kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ + kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ + kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ + kernel/modops.cmi +kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ + kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ + kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ + kernel/modops.cmi kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi kernel/mod_subst.cmi kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ @@ -744,24 +757,22 @@ kernel/mod_typing.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ kernel/term_typing.cmi kernel/subtyping.cmi kernel/reduction.cmi \ kernel/names.cmi kernel/modops.cmi kernel/mod_subst.cmi \ kernel/environ.cmi kernel/entries.cmi kernel/declarations.cmi \ - kernel/cemitcodes.cmi kernel/cbytegen.cmi kernel/mod_typing.cmi + kernel/cemitcodes.cmi kernel/mod_typing.cmi kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/term_typing.cmx kernel/subtyping.cmx kernel/reduction.cmx \ kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \ kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \ - kernel/cemitcodes.cmx kernel/cbytegen.cmx kernel/mod_typing.cmi -kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \ - kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \ - kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \ - kernel/cbytegen.cmi kernel/modops.cmi -kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ - kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ - kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ - kernel/cbytegen.cmx kernel/modops.cmi + kernel/cemitcodes.cmx kernel/mod_typing.cmi kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/options.cmi \ lib/hashcons.cmi kernel/names.cmi kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/options.cmx \ lib/hashcons.cmx kernel/names.cmi +kernel/pre_env.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ + kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi \ + kernel/pre_env.cmi +kernel/pre_env.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \ + kernel/sign.cmx kernel/names.cmx kernel/declarations.cmx \ + kernel/pre_env.cmi kernel/reduction.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/sign.cmi kernel/names.cmi kernel/esubst.cmi kernel/environ.cmi \ kernel/declarations.cmi kernel/conv_oracle.cmi kernel/closure.cmi \ @@ -805,13 +816,13 @@ kernel/term_typing.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ kernel/reduction.cmi kernel/names.cmi kernel/inductive.cmi \ kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \ kernel/declarations.cmi kernel/cooking.cmi kernel/cemitcodes.cmi \ - kernel/cbytegen.cmi kernel/term_typing.cmi + kernel/term_typing.cmi kernel/term_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/type_errors.cmx kernel/term.cmx kernel/sign.cmx \ kernel/reduction.cmx kernel/names.cmx kernel/inductive.cmx \ kernel/indtypes.cmx kernel/environ.cmx kernel/entries.cmx \ kernel/declarations.cmx kernel/cooking.cmx kernel/cemitcodes.cmx \ - kernel/cbytegen.cmx kernel/term_typing.cmi + kernel/term_typing.cmi kernel/type_errors.cmo: kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi \ kernel/names.cmi kernel/environ.cmi kernel/type_errors.cmi kernel/type_errors.cmx: kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx \ @@ -831,13 +842,11 @@ kernel/univ.cmx: lib/util.cmx lib/pp.cmx kernel/names.cmx lib/hashcons.cmx \ kernel/vconv.cmo: kernel/vm.cmi lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/reduction.cmi kernel/names.cmi kernel/inductive.cmi \ kernel/environ.cmi kernel/declarations.cmi kernel/csymtable.cmi \ - kernel/conv_oracle.cmi kernel/closure.cmi kernel/cbytecodes.cmi \ - kernel/vconv.cmi + kernel/conv_oracle.cmi kernel/closure.cmi kernel/vconv.cmi kernel/vconv.cmx: kernel/vm.cmx lib/util.cmx kernel/univ.cmx kernel/term.cmx \ kernel/reduction.cmx kernel/names.cmx kernel/inductive.cmx \ kernel/environ.cmx kernel/declarations.cmx kernel/csymtable.cmx \ - kernel/conv_oracle.cmx kernel/closure.cmx kernel/cbytecodes.cmx \ - kernel/vconv.cmi + kernel/conv_oracle.cmx kernel/closure.cmx kernel/vconv.cmi kernel/vm.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \ kernel/conv_oracle.cmi kernel/cbytecodes.cmi kernel/vm.cmi kernel/vm.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \ @@ -852,10 +861,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmap.cmo: lib/gmap.cmi -lib/gmap.cmx: lib/gmap.cmi lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi +lib/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi @@ -864,24 +873,14 @@ lib/heap.cmo: lib/heap.cmi lib/heap.cmx: lib/heap.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi -lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi +lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi -lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi -lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi -lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi -lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \ kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \ @@ -996,6 +995,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \ library/lib.cmx library/states.cmi library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi +lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi +lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi +lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi +lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \ interp/genarg.cmi parsing/ast.cmi @@ -1318,12 +1327,12 @@ parsing/tactic_printer.cmo: lib/util.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ parsing/printer.cmi translate/pptacticnew.cmi parsing/pptactic.cmi \ lib/pp.cmi lib/options.cmi proofs/logic.cmi library/global.cmi \ - pretyping/evd.cmi parsing/tactic_printer.cmi + pretyping/evd.cmi kernel/environ.cmi parsing/tactic_printer.cmi parsing/tactic_printer.cmx: lib/util.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ parsing/printer.cmx translate/pptacticnew.cmx parsing/pptactic.cmx \ lib/pp.cmx lib/options.cmx proofs/logic.cmx library/global.cmx \ - pretyping/evd.cmx parsing/tactic_printer.cmi + pretyping/evd.cmx kernel/environ.cmx parsing/tactic_printer.cmi parsing/termast.cmo: lib/util.cmi kernel/univ.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi pretyping/reductionops.cmi \ pretyping/rawterm.cmi lib/pp.cmi pretyping/pattern.cmi \ @@ -1787,8 +1796,8 @@ tactics/autorewrite.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi kernel/names.cmi \ kernel/mod_subst.cmi library/libobject.cmi library/lib.cmi \ tactics/hipattern.cmi library/global.cmi pretyping/evd.cmi \ - tactics/equality.cmi parsing/coqast.cmi parsing/ast.cmi \ - tactics/autorewrite.cmi + tactics/equality.cmi kernel/environ.cmi parsing/coqast.cmi \ + parsing/ast.cmi tactics/autorewrite.cmi tactics/autorewrite.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/typing.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ @@ -1796,8 +1805,8 @@ tactics/autorewrite.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx kernel/names.cmx \ kernel/mod_subst.cmx library/libobject.cmx library/lib.cmx \ tactics/hipattern.cmx library/global.cmx pretyping/evd.cmx \ - tactics/equality.cmx parsing/coqast.cmx parsing/ast.cmx \ - tactics/autorewrite.cmi + tactics/equality.cmx kernel/environ.cmx parsing/coqast.cmx \ + parsing/ast.cmx tactics/autorewrite.cmi tactics/btermdn.cmo: tactics/termdn.cmi kernel/term.cmi pretyping/pattern.cmi \ library/libnames.cmi tactics/dn.cmi tactics/btermdn.cmi tactics/btermdn.cmx: tactics/termdn.cmx kernel/term.cmx pretyping/pattern.cmx \ @@ -1913,11 +1922,13 @@ tactics/equality.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/univ.cmx \ tactics/evar_tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi proofs/proof_type.cmi pretyping/evd.cmi \ - pretyping/evarutil.cmi proofs/evar_refiner.cmi tactics/evar_tactics.cmi + pretyping/evarutil.cmi proofs/evar_refiner.cmi kernel/environ.cmi \ + tactics/evar_tactics.cmi tactics/evar_tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx proofs/tacmach.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx proofs/proof_type.cmx pretyping/evd.cmx \ - pretyping/evarutil.cmx proofs/evar_refiner.cmx tactics/evar_tactics.cmi + pretyping/evarutil.cmx proofs/evar_refiner.cmx kernel/environ.cmx \ + tactics/evar_tactics.cmi tactics/extraargs.cmo: lib/util.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ tactics/setoid_replace.cmi parsing/pptactic.cmi parsing/ppconstr.cmi \ lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \ @@ -2247,7 +2258,7 @@ toplevel/coqtop.cmo: kernel/vm.cmi toplevel/vernac.cmi kernel/vconv.cmi \ library/states.cmi lib/profile.cmi lib/pp.cmi lib/options.cmi \ kernel/names.cmi library/nameops.cmi toplevel/mltop.cmi \ library/library.cmi library/libnames.cmi library/lib.cmi \ - library/global.cmi kernel/environ.cmi library/declaremods.cmi \ + library/global.cmi library/declaremods.cmi kernel/declarations.cmi \ toplevel/coqinit.cmi config/coq_config.cmi toplevel/cerrors.cmi \ toplevel/coqtop.cmi toplevel/coqtop.cmx: kernel/vm.cmx toplevel/vernac.cmx kernel/vconv.cmx \ @@ -2255,7 +2266,7 @@ toplevel/coqtop.cmx: kernel/vm.cmx toplevel/vernac.cmx kernel/vconv.cmx \ library/states.cmx lib/profile.cmx lib/pp.cmx lib/options.cmx \ kernel/names.cmx library/nameops.cmx toplevel/mltop.cmx \ library/library.cmx library/libnames.cmx library/lib.cmx \ - library/global.cmx kernel/environ.cmx library/declaremods.cmx \ + library/global.cmx library/declaremods.cmx kernel/declarations.cmx \ toplevel/coqinit.cmx config/coq_config.cmx toplevel/cerrors.cmx \ toplevel/coqtop.cmi toplevel/discharge.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ @@ -2362,20 +2373,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.cmx \ toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi -toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ - proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ - parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ - library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ - interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ - proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ - parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ - library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ - interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \ kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ @@ -2438,6 +2435,20 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ parsing/extend.cmx parsing/coqast.cmx parsing/ast.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi lib/system.cmi library/states.cmi \ + proofs/refiner.cmi translate/ppvernacnew.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi lib/options.cmi kernel/names.cmi library/library.cmi \ + library/lib.cmi parsing/lexer.cmi parsing/coqast.cmi \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx lib/system.cmx library/states.cmx \ + proofs/refiner.cmx translate/ppvernacnew.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx lib/options.cmx kernel/names.cmx library/library.cmx \ + library/lib.cmx parsing/lexer.cmx parsing/coqast.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/vernac.cmi toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi kernel/term.cmi \ lib/system.cmi interp/syntax_def.cmi pretyping/rawterm.cmi lib/pp.cmi \ parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ @@ -2527,15 +2538,17 @@ contrib/cc/cctac.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacinterp.cmi kernel/sign.cmi proofs/proof_type.cmi lib/pp.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ pretyping/inductiveops.cmi library/global.cmi pretyping/evd.cmi \ - kernel/declarations.cmi interp/coqlib.cmi kernel/closure.cmi \ - contrib/cc/ccproof.cmi contrib/cc/ccalgo.cmi contrib/cc/cctac.cmi + kernel/environ.cmi kernel/declarations.cmi interp/coqlib.cmi \ + kernel/closure.cmi contrib/cc/ccproof.cmi contrib/cc/ccalgo.cmi \ + contrib/cc/cctac.cmi contrib/cc/cctac.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx kernel/sign.cmx proofs/proof_type.cmx lib/pp.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ pretyping/inductiveops.cmx library/global.cmx pretyping/evd.cmx \ - kernel/declarations.cmx interp/coqlib.cmx kernel/closure.cmx \ - contrib/cc/ccproof.cmx contrib/cc/ccalgo.cmx contrib/cc/cctac.cmi + kernel/environ.cmx kernel/declarations.cmx interp/coqlib.cmx \ + kernel/closure.cmx contrib/cc/ccproof.cmx contrib/cc/ccalgo.cmx \ + contrib/cc/cctac.cmi contrib/cc/g_congruence.cmo: lib/util.cmi tactics/tactics.cmi \ tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ proofs/refiner.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \ @@ -2546,6 +2559,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \ proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \ lib/options.cmx interp/genarg.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx contrib/cc/cctac.cmx +contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ + kernel/sign.cmi kernel/names.cmi library/global.cmi \ + contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ + kernel/sign.cmx kernel/names.cmx library/global.cmx \ + contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \ @@ -2560,12 +2579,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ library/libnames.cmx kernel/indtypes.cmx library/global.cmx \ kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \ kernel/declarations.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \ - kernel/sign.cmi kernel/names.cmi library/global.cmi \ - contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \ - kernel/sign.cmx kernel/names.cmx library/global.cmx \ - contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \ library/nametab.cmi kernel/names.cmi library/global.cmi \ interp/constrintern.cmi contrib/correctness/pdb.cmi @@ -2688,6 +2701,8 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \ contrib/correctness/pwp.cmi +contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi +contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi library/summary.cmi translate/ppconstrnew.cmi \ @@ -2706,8 +2721,6 @@ contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ contrib/dp/dp_zenon.cmx contrib/dp/dp_sorts.cmx \ contrib/dp/dp_simplify.cmx contrib/dp/dp_cvcl.cmx kernel/declarations.cmx \ interp/coqlib.cmx contrib/dp/dp.cmi -contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi -contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi @@ -3192,6 +3205,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \ proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \ library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ interp/coqlib.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ + contrib/interface/vtp.cmi contrib/interface/translate.cmi \ + parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ + parsing/esyntax.cmi contrib/interface/ascent.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ + contrib/interface/vtp.cmx contrib/interface/translate.cmx \ + parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ + parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi parsing/termast.cmi kernel/term.cmi \ @@ -3216,14 +3237,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/evd.cmx kernel/environ.cmx kernel/declarations.cmx \ parsing/coqast.cmx interp/constrintern.cmx pretyping/clenv.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \ - contrib/interface/vtp.cmi contrib/interface/translate.cmi \ - parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \ - parsing/esyntax.cmi contrib/interface/ascent.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ - contrib/interface/vtp.cmx contrib/interface/translate.cmx \ - parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ - parsing/esyntax.cmx contrib/interface/ascent.cmi contrib/interface/translate.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \ parsing/termast.cmi kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi \ @@ -3447,13 +3460,15 @@ contrib/rtauto/refl_tauto.cmo: lib/util.cmi pretyping/termops.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi lib/system.cmi \ pretyping/retyping.cmi contrib/rtauto/proof_search.cmi lib/pp.cmi \ kernel/names.cmi library/goptions.cmi lib/explore.cmi pretyping/evd.cmi \ - interp/coqlib.cmi kernel/closure.cmi contrib/rtauto/refl_tauto.cmi + kernel/environ.cmi interp/coqlib.cmi kernel/closure.cmi \ + contrib/rtauto/refl_tauto.cmi contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx proofs/tactic_debug.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx lib/system.cmx \ pretyping/retyping.cmx contrib/rtauto/proof_search.cmx lib/pp.cmx \ kernel/names.cmx library/goptions.cmx lib/explore.cmx pretyping/evd.cmx \ - interp/coqlib.cmx kernel/closure.cmx contrib/rtauto/refl_tauto.cmi + kernel/environ.cmx interp/coqlib.cmx kernel/closure.cmx \ + contrib/rtauto/refl_tauto.cmi contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ @@ -3482,14 +3497,14 @@ contrib/subtac/eterm.cmo: pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ contrib/subtac/sutils.cmi kernel/reduction.cmi lib/pp.cmi \ kernel/names.cmi library/global.cmi pretyping/evd.cmi \ - pretyping/evarutil.cmi library/declare.cmi library/decl_kinds.cmo \ - contrib/subtac/eterm.cmi + pretyping/evarutil.cmi kernel/environ.cmi library/declare.cmi \ + library/decl_kinds.cmo contrib/subtac/eterm.cmi contrib/subtac/eterm.cmx: pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ contrib/subtac/sutils.cmx kernel/reduction.cmx lib/pp.cmx \ kernel/names.cmx library/global.cmx pretyping/evd.cmx \ - pretyping/evarutil.cmx library/declare.cmx library/decl_kinds.cmx \ - contrib/subtac/eterm.cmi + pretyping/evarutil.cmx kernel/environ.cmx library/declare.cmx \ + library/decl_kinds.cmx contrib/subtac/eterm.cmi contrib/subtac/g_eterm.cmo: lib/util.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi lib/options.cmi \ @@ -3554,18 +3569,12 @@ contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \ parsing/egrammar.cmx parsing/coqast.cmx toplevel/cerrors.cmx contrib/subtac/sutils.cmo: contrib/subtac/sutils.cmi contrib/subtac/sutils.cmx: contrib/subtac/sutils.cmi -contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi -contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \ kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \ kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx -contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ - tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ - contrib/xml/acic.cmo -contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ - tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ - contrib/xml/acic.cmx +contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi +contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \ @@ -3584,6 +3593,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \ kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \ library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \ contrib/xml/acic.cmx +contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \ + tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/acic.cmo +contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \ + tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \ + contrib/xml/acic.cmx contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \ kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ @@ -3603,13 +3618,13 @@ contrib/xml/doubleTypeInference.cmx: lib/util.cmx contrib/xml/unshare.cmx \ contrib/xml/proof2aproof.cmo: lib/util.cmi contrib/xml/unshare.cmi \ pretyping/termops.cmi kernel/term.cmi parsing/tactic_printer.cmi \ proofs/tacmach.cmi kernel/sign.cmi proofs/refiner.cmi \ - proofs/proof_type.cmi lib/pp.cmi proofs/logic.cmi library/global.cmi \ - pretyping/evd.cmi pretyping/evarutil.cmi + proofs/proof_type.cmi lib/pp.cmi proofs/logic.cmi pretyping/evd.cmi \ + pretyping/evarutil.cmi kernel/environ.cmi contrib/xml/proof2aproof.cmx: lib/util.cmx contrib/xml/unshare.cmx \ pretyping/termops.cmx kernel/term.cmx parsing/tactic_printer.cmx \ proofs/tacmach.cmx kernel/sign.cmx proofs/refiner.cmx \ - proofs/proof_type.cmx lib/pp.cmx proofs/logic.cmx library/global.cmx \ - pretyping/evd.cmx pretyping/evarutil.cmx + proofs/proof_type.cmx lib/pp.cmx proofs/logic.cmx pretyping/evd.cmx \ + pretyping/evarutil.cmx kernel/environ.cmx contrib/xml/proofTree2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi \ contrib/xml/unshare.cmi kernel/term.cmi proofs/tacexpr.cmo \ kernel/sign.cmi proofs/proof_type.cmi contrib/xml/proof2aproof.cmo \ @@ -3626,8 +3641,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \ contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \ lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \ pretyping/recordops.cmi proofs/proof_trees.cmi \ @@ -3658,10 +3671,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx -ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ - ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi -ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ - ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \ ide/utils/configwin_ihm.cmo @@ -3672,6 +3683,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \ ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \ ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx +ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \ + ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi +ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \ + ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \ @@ -3813,176 +3828,74 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ + kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h @@ -130,11 +130,11 @@ KERNEL=\ kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ kernel/cbytecodes.cmo kernel/copcodes.cmo \ kernel/cemitcodes.cmo kernel/vm.cmo \ - kernel/declarations.cmo kernel/environ.cmo kernel/conv_oracle.cmo \ - kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo\ - kernel/entries.cmo \ - kernel/cbytegen.cmo kernel/csymtable.cmo \ - kernel/modops.cmo \ + kernel/declarations.cmo kernel/pre_env.cmo \ + kernel/cbytegen.cmo kernel/environ.cmo \ + kernel/csymtable.cmo kernel/conv_oracle.cmo \ + kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo \ + kernel/entries.cmo kernel/modops.cmo \ kernel/inductive.cmo kernel/vconv.cmo kernel/typeops.cmo \ kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \ kernel/subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo @@ -1398,10 +1398,10 @@ GRAMMARNEEDEDCMO=\ kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ - kernel/declarations.cmo kernel/environ.cmo kernel/conv_oracle.cmo \ + kernel/declarations.cmo kernel/pre_env.cmo \ + kernel/cbytegen.cmo kernel/conv_oracle.cmo kernel/environ.cmo \ kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo\ kernel/entries.cmo \ - kernel/cbytegen.cmo \ kernel/modops.cmo \ kernel/inductive.cmo kernel/typeops.cmo \ kernel/indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo \ @@ -1433,9 +1433,10 @@ PRINTERSCMO=\ config/coq_config.cmo lib/lib.cma \ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ kernel/mod_subst.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ - kernel/sign.cmo kernel/declarations.cmo kernel/environ.cmo \ + kernel/sign.cmo kernel/declarations.cmo kernel/pre_env.cmo \ + kernel/cbytecodes.cmo kernel/cbytegen.cmo kernel/environ.cmo \ kernel/conv_oracle.cmo kernel/closure.cmo kernel/reduction.cmo \ - kernel/cooking.cmo kernel/cbytecodes.cmo kernel/cbytegen.cmo \ + kernel/cooking.cmo \ kernel/modops.cmo kernel/type_errors.cmo kernel/inductive.cmo \ kernel/subtyping.cmo kernel/typeops.cmo kernel/indtypes.cmo \ kernel/term_typing.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo \ diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 71545d966..a3e1902c0 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -131,7 +131,7 @@ let rec make_prb gls additionnal_terms = add_disequality state (HeqnH (idp,id)) ph nh) !pos_hyps; neg_hyps:=(id,nh):: !neg_hyps - end) gls.it.evar_hyps; + end) (Environ.named_context_of_val gls.it.evar_hyps); begin match atom_of_constr env gls.it.evar_concl with `Eq (t,a,b) -> add_disequality state Goal a b diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6bc667339..41619c85f 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -354,7 +354,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let rec names_prod t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t - | Cast(t,_) -> names_prod t + | Cast(t,_,_) -> names_prod t | _ -> [] in let field_names = @@ -515,7 +515,7 @@ let rec extract_term env mle mlt c args = extract_app env mle mlt (extract_fix env mle i recd) args | CoFix (i,recd) -> extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c, _) -> extract_term env mle mlt c args + | Cast (c,_,_) -> extract_term env mle mlt c args | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 657d4cba5..fb75655f0 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -91,8 +91,8 @@ let compare_constr_int f t1 t2 = | Meta m1, Meta m2 -> m1 - m2 | Var id1, Var id2 -> Pervasives.compare id1 id2 | Sort s1, Sort s2 -> Pervasives.compare s1 s2 - | Cast (c1,_), _ -> f c1 t2 - | _, Cast (c2,_) -> f t1 c2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) | Lambda (_,t1,c1), Lambda (_,t2,c2) -> (f =? f) t1 t2 c1 c2 diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml index a1e620a23..41a100c2b 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/first-order/unify.ml @@ -59,8 +59,8 @@ let unif t1 t2= if Intset.is_empty (free_rels t) && not (occur_term (mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) - | Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige - | _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 5e31d5675..e40cd2676 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -85,13 +85,13 @@ let string_of_R_constant kn = let rec string_of_R_constr c = match kind_of_term c with - Cast (c,t) -> string_of_R_constr c + Cast (c,_,_) -> string_of_R_constr c |Const c -> string_of_R_constant c | _ -> "not_of_constant" let rec rational_of_constr c = match kind_of_term c with - | Cast (c,t) -> (rational_of_constr c) + | Cast (c,_,_) -> (rational_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with | "Ropp" -> @@ -122,7 +122,7 @@ let rec rational_of_constr c = let rec flin_of_constr c = try( match kind_of_term c with - | Cast (c,t) -> (flin_of_constr c) + | Cast (c,_,_) -> (flin_of_constr c) | App (c,args) -> (match (string_of_R_constr c) with "Ropp" -> diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 27f14aedf..064f279f0 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -74,7 +74,7 @@ let rec mkevarmap_from_listex lex = let _ = prconstr typ in*) let info ={ evar_concl = typ; - evar_hyps = empty_named_context; + evar_hyps = empty_named_context_val; evar_body = Evar_empty} in Evd.add (mkevarmap_from_listex lex') ex info diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 09b918be5..807883115 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -93,7 +93,7 @@ let rec def_const_in_term_rec vl x = def_const_in_term_rec vl (mkInd (inductive_of_constructor c)) | Case(_,x,t,a) -> def_const_in_term_rec vl x - | Cast(x,t)-> def_const_in_term_rec vl t + | Cast(x,_,t)-> def_const_in_term_rec vl t | Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x) ;; diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 532955661..f8328f21d 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -106,7 +106,7 @@ let make_final_cmd f optname clear_names constr path = add_clear_names_if_necessary (f optname constr path) clear_names;; let (rem_cast:pbp_rule) = function - (a,c,cf,o, Cast(f,_), p, func) -> + (a,c,cf,o, Cast(f,_,_), p, func) -> Some(func a c cf o (kind_of_term f) p) | _ -> None;; diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 2560b0b82..1c89156b5 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -54,7 +54,7 @@ and ngoal= {newhyp : nhyp list; t_concl : Term.constr; t_full_concl: Term.constr; - t_full_env: Sign.named_context} + t_full_env: Environ.named_context_val} and ntree= {t_info:string; t_goal:ngoal; @@ -151,7 +151,7 @@ let seq_to_lnhyp sign sign' cl = {newhyp=nh; t_concl=cl; t_full_concl=long_type_hyp !lh cl; - t_full_env = sign@sign'} + t_full_env = Environ.val_of_named_context (sign@sign')} ;; @@ -247,6 +247,7 @@ let old_sign osign sign = let to_nproof sigma osign pf = let rec to_nproof_rec sigma osign pf = let {evar_hyps=sign;evar_concl=cl} = pf.goal in + let sign = Environ.named_context_of_val sign in let nsign = new_sign osign sign in let oldsign = old_sign osign sign in match pf.ref with @@ -759,7 +760,7 @@ let rec nsortrec vl x = nsortrec vl (mkInd (inductive_of_constructor c)) | Case(_,x,t,a) -> nsortrec vl x - | Cast(x,t)-> nsortrec vl t + | Cast(x,_, t)-> nsortrec vl t | Const c -> nsortrec vl (lookup_constant c vl).const_type | _ -> nsortrec vl (type_of vl Evd.empty x) ;; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 391cc0f7c..69c6674d3 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -411,7 +411,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CDynamic (_, _) -> assert false | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula num) - | CCast (_, e, t) -> + | CCast (_, e,_, t) -> CT_coerce_TYPED_FORMULA_to_FORMULA (CT_typed_formula(xlate_formula e, xlate_formula t)) | CPatVar (_, (_,i)) when is_int_meta i -> diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 30562cd44..46b987112 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -460,7 +460,7 @@ type constr_path = let context operation path (t : constr) = let rec loop i p0 t = match (p0,kind_of_term t) with - | (p, Cast (c,t)) -> mkCast (loop i p c,t) + | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t) | ([], _) -> operation i t | ((P_APP n :: p), App (f,v)) -> let v' = Array.copy v in @@ -498,7 +498,7 @@ let context operation path (t : constr) = let occurence path (t : constr) = let rec loop p0 t = match (p0,kind_of_term t) with - | (p, Cast (c,t)) -> loop p c + | (p, Cast (c,_,_)) -> loop p c | ([], _) -> t | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n) | ((P_BRANCH n :: p), Case (_,_,_,v)) -> loop p v.(n) @@ -524,7 +524,7 @@ let abstract_path typ path t = let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl_no_check newc gl + convert_concl_no_check newc DEFAULTcast gl let focused_simpl path = simpl_time (focused_simpl path) diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index aa7766785..4121580ff 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -132,7 +132,7 @@ let rec (find_call_occs: | Meta(_) -> error "find_call_occs : Meta" | Evar(_) -> error "find_call_occs : Evar" | Sort(_) -> error "find_call_occs : Sort" - | Cast(_,_) -> error "find_call_occs : cast" + | Cast(_,_,_) -> error "find_call_occs : cast" | Prod(_,_,_) -> error "find_call_occs : Prod" | Lambda(_,_,_) -> error "find_call_occs : Lambda" | LetIn(_,_,_,_) -> error "find_call_occs : let in" @@ -514,7 +514,7 @@ let com_terminate fonctional_ref input_type relation_ast wf_thm_ast let (proofs_constr:constr list) = List.map (fun x -> interp_constr evmap env x) proofs in (start_proof thm_name - (IsGlobal (Proof Lemma)) (Environ.named_context env) (hyp_terminates fonctional_ref) + (IsGlobal (Proof Lemma)) (Environ.named_context_val env) (hyp_terminates fonctional_ref) (fun _ _ -> ()); by (whole_start fonctional_ref input_type relation wf_thm proofs_constr); @@ -713,7 +713,7 @@ let (com_eqn : identifier -> let eq_constr = interp_constr evmap env eq in let f_constr = (constr_of_reference f_ref) in (start_proof eq_name (IsGlobal (Proof Lemma)) - (Environ.named_context env) eq_constr (fun _ _ -> ()); + (Environ.named_context_val env) eq_constr (fun _ _ -> ()); by (start_equation f_ref terminate_ref (fun x -> diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index fb0e66526..3b937c7a6 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -212,7 +212,7 @@ let compute_rhs bodyi index_of_f = PMeta (Some (coerce_meta_in i)) | App (f,args) -> PApp (pattern_of_constr f, Array.map aux args) - | Cast (c,t) -> aux c + | Cast (c,_,_) -> aux c | _ -> pattern_of_constr c in aux bodyi @@ -297,7 +297,7 @@ binary search trees (see file \texttt{Quote.v}) *) let rec closed_under cset t = (ConstrSet.mem t cset) or (match (kind_of_term t) with - | Cast(c,_) -> closed_under cset c + | Cast(c,_,_) -> closed_under cset c | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l | _ -> false) @@ -360,7 +360,7 @@ let rec subterm gl (t : constr) (t' : constr) = (pf_conv_x gl t t') or (match (kind_of_term t) with | App (f,args) -> array_exists (fun t -> subterm gl t t') args - | Cast(t,_) -> (subterm gl t t') + | Cast(t,_,_) -> (subterm gl t t') | _ -> false) (*s We want to sort the list according to reverse subterm order. *) @@ -447,8 +447,8 @@ let quote f lid gl = | _ -> assert false in match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl + | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl + | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl (*i diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index d3068c862..4884f23c6 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -773,7 +773,7 @@ open RedFlags let polynom_unfold_tac = let flags = (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in - reduct_in_concl (cbv_norm_flags flags) + reduct_in_concl (cbv_norm_flags flags,DEFAULTcast) let polynom_unfold_tac_in_term gl = let flags = diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v index d1cb80275..342c03dba 100644 --- a/contrib/rtauto/Rtauto.v +++ b/contrib/rtauto/Rtauto.v @@ -18,7 +18,7 @@ Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. Ltac clean:=try (simpl;congruence). Inductive form:Set:= -Atom : positive -> form + Atom : positive -> form | Arrow : form -> form -> form | Bot | Conjunct : form -> form -> form @@ -395,4 +395,4 @@ exact (Reflect (empty \ A \ B \ C) (I_Or_r (I_And (Ax 2) (Ax 4))))))). Qed. Print toto. -*)
\ No newline at end of file +*) diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml index 0865a825c..801122476 100644 --- a/contrib/rtauto/refl_tauto.ml +++ b/contrib/rtauto/refl_tauto.ml @@ -113,7 +113,7 @@ let rec make_form atom_env gls term = Arrow (fa,fb) else make_atom atom_env (normalize term) - | Cast(a,b) -> + | Cast(a,_,_) -> make_form atom_env gls a | Ind ind -> if ind = Lazy.force li_False then @@ -273,7 +273,8 @@ let rtauto_tac gls= (pf_env gls) (Tacmach.project gls) gl <> InProp then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] gls.it.evar_hyps in + let hyps=make_hyps gamma gls [gl] + (Environ.named_context_of_val gls.it.evar_hyps) in let formula= List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in let search_fun = diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index d98b3b6bd..6c3f87a5b 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -164,7 +164,7 @@ Ltac Make_ring_rw Cst_tac lemma req r := let pe1 := mkPol r1 fv in let pe2 := mkPol r2 fv in ((apply (lemma1 fv pe1 pe2); - compute; + vm_compute; exact (refl_equal true)) || (Make_ring_rewrite_step (lemma2 fv) pe1; Make_ring_rewrite_step (lemma2 fv) pe2)) diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 573f83cea..6a78e88c7 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -195,10 +195,10 @@ let protect_red env sigma c = (mk_clos_but (is_ring_thm req) c);; let protect_tac = - Tactics.reduct_option protect_red None ;; + Tactics.reduct_option (protect_red,DEFAULTcast) None ;; let protect_tac_in id = - Tactics.reduct_option protect_red (Some(id,[],(InHyp, ref None)));; + Tactics.reduct_option (protect_red,DEFAULTcast) (Some(id,[],(InHyp, ref None)));; TACTIC EXTEND protect_fv diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 4f86af1e8..7b07abbc8 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -61,7 +61,7 @@ let etype_of_evar evs ev = | [] -> let t' = subst_evars evs n ev.evar_concl in subst_vars acc 0 t' - in aux [] 0 (rev ev.evar_hyps) + in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps)) open Tacticals diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml index dcca9361a..876dc68bb 100644 --- a/contrib/subtac/infer.ml +++ b/contrib/subtac/infer.ml @@ -552,7 +552,7 @@ let rec dtype_of_types ctx c = | Meta mv -> notimpl "Meta" | Evar pex -> notimpl "Evar" | Sort s -> DTSort (dummy_loc, s) - | Cast (c, t) -> snd (dtype_of_types ctx t) + | Cast (c, _, t) -> snd (dtype_of_types ctx t) | Prod (n, t, t') -> let dt = dtype_of_types ctx t in let ctx' = (n, dt) :: ctx in @@ -600,7 +600,7 @@ let rec dtype_of_constr ctx c = | Meta mv -> notimpl "Meta" | Evar pex -> notimpl "Evar" | Sort s -> DTSort (dummy_loc, s) - | Cast (c, t) -> snd (dtype_of_constr ctx t) + | Cast (_,_,t) -> snd (dtype_of_constr ctx t) | Prod (n, t, t') -> let dt = dtype_of_constr ctx t in let ctx' = (n, dt) :: ctx in diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml index c9a0a78c7..ce0f15ec2 100644 --- a/contrib/subtac/rewrite.ml +++ b/contrib/subtac/rewrite.ml @@ -349,7 +349,8 @@ and subset_coerce prog_info ctx x y = let ctx', pcx' = subst_ctx ctx pcx in cx, { Evd.evar_concl = pcx'; - Evd.evar_hyps = evar_ctx prog_info ctx'; + Evd.evar_hyps = + Environ.val_of_named_context (evar_ctx prog_info ctx'); Evd.evar_body = Evd.Evar_empty; } in @@ -368,7 +369,7 @@ and subset_coerce prog_info ctx x y = in ignore(Univ.merge_constraints cstrs (Global.universes ())); Some (fun x -> - mkCast (x, y)) + mkCast (x, DEFAULTcast, y)) with Reduction.NotConvertible -> subtyping_error @@ -420,7 +421,9 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types = let evarinfo = { Evd.evar_concl = proof; - Evd.evar_hyps = evar_ctx prog_info ctx'; + Evd.evar_hyps = + Environ.val_of_named_context + (evar_ctx prog_info ctx'); Evd.evar_body = Evd.Evar_empty; } in @@ -581,7 +584,7 @@ let subtac recursive id (s, t) = let key = mknewexist () in prog_info.evm <- Evd.add prog_info.evm key { Evd.evar_concl = wf_rel; - Evd.evar_hyps = []; + Evd.evar_hyps = Environ.empty_named_context_val; Evd.evar_body = Evd.Evar_empty }; mkEvar (key, [| |]) in diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 54510ba17..caac70310 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -263,7 +263,7 @@ let typeur sigma metamap = | T.App(f,args)-> T.strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) - | T.Cast (c,t) -> t + | T.Cast (c,_, t) -> t | T.Sort _ | T.Prod _ -> match sort_of env cstr with Coq_sort T.InProp -> T.mkProp @@ -273,7 +273,7 @@ let typeur sigma metamap = and sort_of env t = match Term.kind_of_term t with - | T.Cast (c,s) when T.isSort s -> family_of_term s + | T.Cast (c,_, s) when T.isSort s -> family_of_term s | T.Sort (T.Prop c) -> Coq_sort T.InType | T.Sort (T.Type u) -> Coq_sort T.InType | T.Prod (name,t,c2) -> @@ -283,7 +283,7 @@ let typeur sigma metamap = | Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s | Coq_sort T.InType, (Coq_sort T.InSet as s) | CProp, (Coq_sort T.InSet as s) when - Environ.engagement env = Some Environ.ImpredicativeSet -> s + Environ.engagement env = Some Declarations.ImpredicativeSet -> s | Coq_sort T.InType, Coq_sort T.InSet | CProp, Coq_sort T.InSet -> Coq_sort T.InType | _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*) @@ -295,7 +295,7 @@ let typeur sigma metamap = and sort_family_of env t = match T.kind_of_term t with - | T.Cast (c,s) when T.isSort s -> family_of_term s + | T.Cast (c,_, s) when T.isSort s -> family_of_term s | T.Sort (T.Prop c) -> Coq_sort T.InType | T.Sort (T.Type u) -> Coq_sort T.InType | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2 @@ -560,7 +560,7 @@ print_endline "PASSATO" ; flush stdout ; (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) | T.Meta _ -> Util.anomaly "Meta met during exporting to XML" | T.Sort s -> A.ASort (fresh_id'', s) - | T.Cast (v,t) -> + | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index d4093f002..24676f186 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -42,7 +42,7 @@ prerr_endline "###whd_betadeltaiotacprop:" ; let xxx = (*Pp.msgerr (Printer.prterm_env env ty);*) prerr_endline ""; - Redexpr.reduction_of_red_expr red_exp env evar_map ty + (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty in prerr_endline "###FINE" ; (* @@ -92,7 +92,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let ty = Unshare.unshare (Evd.existential_type sigma ev) in let jty = execute env sigma ty None in let jty = assumption_of_judgment env sigma jty in - let evar_context = (Evd.map sigma n).Evd.evar_hyps in + let evar_context = + E.named_context_of_val (Evd.map sigma n).Evd.evar_hyps in let rec iter actual_args evar_context = match actual_args,evar_context with [],[] -> () @@ -230,11 +231,11 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let j3 = execute env1 sigma c3 None in Typeops.judge_of_letin env name j1 j2 j3 - | T.Cast (c,t) -> + | T.Cast (c,k,t) -> let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in let tj = execute env sigma t None in let tj = type_judgment env sigma tj in - let j, _ = Typeops.judge_of_cast env cj tj in + let j, _ = Typeops.judge_of_cast env cj k tj in j in let synthesized = E.j_type judgement in diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 9220e8a4d..f78df7478 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -32,7 +32,7 @@ let nf_evar sigma ~preserve = match T.kind_of_term t with | T.Rel _ | T.Meta _ | T.Var _ | T.Sort _ | T.Const _ | T.Ind _ | T.Construct _ -> t - | T.Cast (c1,c2) -> T.mkCast (aux c1, aux c2) + | T.Cast (c1,k,c2) -> T.mkCast (aux c1, k, aux c2) | T.Prod (na,c1,c2) -> T.mkProd (na, aux c1, aux c2) | T.Lambda (na,t,c) -> T.mkLambda (na, aux t, aux c) | T.LetIn (na,b,t,c) -> T.mkLetIn (na, aux b, aux t, aux c) @@ -41,7 +41,7 @@ let nf_evar sigma ~preserve = let l' = Array.map aux l in (match T.kind_of_term c' with T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') - | T.Cast (he,_) -> + | T.Cast (he,_,_) -> (match T.kind_of_term he with T.App (c'',l'') -> T.mkApp (c'', Array.append l'' l') | _ -> T.mkApp (c', l') @@ -123,18 +123,22 @@ let extract_open_proof sigma pf = (*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) (*CSC: as the evar_instance. Ordering the instance becomes useless (it *) (*CSC: will already be ordered. *) - (Termops.ids_of_named_context goal.Evd.evar_hyps) in + (Termops.ids_of_named_context + (Environ.named_context_of_val goal.Evd.evar_hyps)) in let sorted_rels = Sort.list (fun (n1,_) (n2,_) -> n1 < n2 ) visible_rels in let context = - List.map - (fun (_,id) -> Sign.lookup_named id goal.Evd.evar_hyps) - sorted_rels + let l = + List.map + (fun (_,id) -> Sign.lookup_named id + (Environ.named_context_of_val goal.Evd.evar_hyps)) + sorted_rels in + Environ.val_of_named_context l in (*CSC: the section variables in the right order must be added too *) let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in - let env = Global.env_of_context context in - let evd',evar = + (* let env = Global.env_of_context context in *) + let evd',evar = Evarutil.new_evar_instance context !evd goal.Evd.evar_concl evar_instance in evd := evd' ; diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 423991784..b9d920903 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -46,7 +46,8 @@ let constr_to_xml obj sigma env = let rel_context = Sign.push_named_to_rel_context named_context' [] in let rel_env = Environ.push_rel_context rel_context - (Environ.reset_with_named_context real_named_context env) in + (Environ.reset_with_named_context + (Environ.val_of_named_context real_named_context) env) in let obj' = Term.subst_vars (List.map (function (i,_,_) -> i) named_context') obj in let seed = ref 0 in @@ -180,11 +181,12 @@ Pp.ppnl (Pp.(++) (Pp.str (constr_to_xml tid sigma env)) >] in let old_names = List.map (fun (id,c,tid)->id) old_hyps in + let nhyps = Environ.named_context_of_val hyps in let new_hyps = - List.filter (fun (id,c,tid)-> not (List.mem id old_names)) hyps in + List.filter (fun (id,c,tid)-> not (List.mem id old_names)) nhyps in X.xml_nempty "Tactic" of_attribute - [<(build_hyps new_hyps) ; (aux flat_proof hyps)>] + [<(build_hyps new_hyps) ; (aux flat_proof nhyps)>] end | {PT.ref=Some(PT.Change_evars,nodes)} -> diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index e8f149402..96f73abe0 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -290,7 +290,7 @@ let find_hyps t = | T.Meta _ | T.Evar _ | T.Sort _ -> l - | T.Cast (te,ty) -> aux (aux l te) ty + | T.Cast (te,_, ty) -> aux (aux l te) ty | T.Prod (_,s,t) -> aux (aux l s) t | T.Lambda (_,s,t) -> aux (aux l s) t | T.LetIn (_,s,_,t) -> aux (aux l s) t @@ -359,7 +359,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env = (* t will not be exported to XML. Thus no unsharing performed *) final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl' in - aux [] (List.rev evar_hyps) + aux [] (List.rev (Environ.named_context_of_val evar_hyps)) in (* We map the named context to a rel context and every Var to a Rel *) (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl)) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 05059bd1b..e8dffb437 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -113,13 +113,19 @@ let pr_obj obj = Format.print_string (Libobject.object_tag obj) let cnt = ref 0 +let cast_kind_display k = + match k with + | VMcast -> "VMcast" + | DEFAULTcast -> "DEFAULTcast" + let constr_display csr = let rec term_display c = match kind_of_term c with | Rel n -> "Rel("^(string_of_int n)^")" | Meta n -> "Meta("^(string_of_int n)^")" | Var id -> "Var("^(string_of_id id)^")" | Sort s -> "Sort("^(sort_display s)^")" - | Cast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")" + | Cast (c,k, t) -> + "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")" | Prod (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" | Lambda (na,t,c) -> @@ -180,7 +186,7 @@ let print_pure_constr csr = | Meta n -> print_string "Meta("; print_int n; print_string ")" | Var id -> print_string (string_of_id id) | Sort s -> sort_display s - | Cast (c,t) -> open_hovbox 1; + | Cast (c,_, t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() | Prod (Name(id),t,c) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1430bdace..7c91eca25 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1052,7 +1052,7 @@ let rec check_same_type ty1 ty2 = | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () | CSort(_,s1), CSort(_,s2) when s1=s2 -> () - | CCast(_,a1,b1), CCast(_,a2,b2) -> + | CCast(_,a1,_,b1), CCast(_,a2,_,b2) -> check_same_type a1 a2; check_same_type b1 b2 | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 -> @@ -1147,8 +1147,8 @@ let rec same_raw c d = | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" | RHole _, _ -> () | _, RHole _ -> () - | RCast(_,c1,_),r2 -> same_raw c1 r2 - | r1, RCast(_,c2,_) -> same_raw r1 c2 + | RCast(_,c1,_,_),r2 -> same_raw c1 r2 + | r1, RCast(_,c2,_,_) -> same_raw r1 c2 | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" | _ -> failwith "same_raw" @@ -1657,8 +1657,8 @@ let rec extern inctx scopes vars r = | RHole (loc,e) -> CHole loc - | RCast (loc,c,t) -> - CCast (loc,sub_extern true scopes vars c,extern_typ scopes vars t) + | RCast (loc,c,k,t) -> + CCast (loc,sub_extern true scopes vars c,k,extern_typ scopes vars t) | RDynamic (loc,d) -> CDynamic (loc,d) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d59d3871d..06d11e665 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -929,8 +929,8 @@ let internalise sigma env allow_soapp lvar c = REvar (loc, n, None) | CSort (loc, s) -> RSort(loc,s) - | CCast (loc, c1, c2) -> - RCast (loc,intern env c1,intern_type env c2) + | CCast (loc, c1, k, c2) -> + RCast (loc,intern env c1,k,intern_type env c2) | CDynamic (loc,d) -> RDynamic (loc,d) diff --git a/interp/reserve.ml b/interp/reserve.ml index 14797930d..917f9f4ad 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -76,7 +76,7 @@ let rec unloc = function bl, Array.map unloc tyl, Array.map unloc bv) - | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t) + | RCast (_,c,k,t) -> RCast (dummy_loc,unloc c,k,unloc t) | RSort (_,x) -> RSort (dummy_loc,x) | RHole (_,x) -> RHole (dummy_loc,x) | RRef (_,x) -> RRef (dummy_loc,x) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index e0f1cc18c..ae6bcd10c 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -46,7 +46,7 @@ type aconstr = | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * aconstr + | ACast of aconstr * cast_kind * aconstr let name_app f e = function | Name id -> let (id, e) = f id e in (e, Name id) @@ -96,7 +96,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function | AIf (c,(na,po),b1,b2) -> let e,na = name_app g e na in RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2) - | ACast (c,t) -> RCast (loc,f e c,f e t) + | ACast (c,k,t) -> RCast (loc,f e c,k,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) | APatVar n -> RPatVar (loc,(false,n)) @@ -196,7 +196,7 @@ let aconstr_and_vars_of_rawconstr a = | RIf (loc,c,(na,po),b1,b2) -> add_name found na; AIf (aux c,(na,option_app aux po),aux b1,aux b2) - | RCast (_,c,t) -> ACast (aux c,aux t) + | RCast (_,c,k,t) -> ACast (aux c,k,aux t) | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w | RRef (_,r) -> ARef r @@ -338,10 +338,10 @@ let rec subst_aconstr subst bound raw = | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw - | ACast (r1,r2) -> + | ACast (r1,k,r2) -> let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ACast (r1',r2') + ACast (r1',k,r2') let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) @@ -423,7 +423,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_ alp metas sigma c1 c2 - | RCast(_,c1,t1), ACast(c2,t2) -> + | RCast(_,c1,_,t1), ACast(c2,_,t2) -> match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 | RSort (_,s1), ASort s2 when s1 = s2 -> sigma | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match @@ -520,7 +520,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * constr_expr + | CCast of loc * constr_expr * cast_kind * constr_expr | CNotation of loc * notation * constr_expr list | CNumeral of loc * Bigint.bigint | CDelimiters of loc * string * constr_expr @@ -569,7 +569,7 @@ let constr_loc = function | CPatVar (loc,_) -> loc | CEvar (loc,_) -> loc | CSort (loc,_) -> loc - | CCast (loc,_,_) -> loc + | CCast (loc,_,_,_) -> loc | CNotation (loc,_,_) -> loc | CNumeral (loc,_) -> loc | CDelimiters (loc,_,_) -> loc @@ -599,7 +599,8 @@ let rec occur_var_constr_expr id = function | CProdN (_,l,b) -> occur_var_binders id b l | CLambdaN (_,l,b) -> occur_var_binders id b l | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a] - | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b + | CCast (loc,a,_,b) -> + occur_var_constr_expr id a or occur_var_constr_expr id b | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l | CDelimiters (loc,_,a) -> occur_var_constr_expr id a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false @@ -621,7 +622,7 @@ and occur_var_binders id b = function let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l) -let mkCastC (a,b) = CCast (dummy_loc,a,b) +let mkCastC (a,k,b) = CCast (dummy_loc,a,k,b) let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) @@ -670,7 +671,7 @@ let map_constr_expr_with_binders f g e = function | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) - | CCast (loc,a,b) -> CCast (loc,f e a,f e b) + | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b) | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 51fcd9c07..0a073c435 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -42,7 +42,7 @@ type aconstr = | ASort of rawsort | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * aconstr + | ACast of aconstr * cast_kind * aconstr val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> @@ -104,7 +104,7 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * constr_expr + | CCast of loc * constr_expr * cast_kind * constr_expr | CNotation of loc * notation * constr_expr list | CNumeral of loc * Bigint.bigint | CDelimiters of loc * string * constr_expr @@ -136,7 +136,7 @@ val names_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr -> constr_expr +val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * constr_expr * constr_expr -> constr_expr diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 48d91e4dc..8bfe78ebe 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */ # define Next break #endif -/*#define _COQ_DEBUG_ */ +/* #define _COQ_DEBUG_ */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) @@ -715,7 +715,7 @@ value coq_interprete forcable = Val_true; /* On pousse l'addresse de retour et l'argument */ sp -= 3; - sp[0] = (value) (pc); + sp[0] = (value) (pc - 1); sp[1] = coq_env; sp[2] = Val_long(coq_extra_args); /* On evalue le cofix */ @@ -966,6 +966,7 @@ value coq_push_vstack(value stk) { value coq_interprete_ml(value tcode, value a, value e, value ea) { print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + print_instr("end coq_interprete"); } value coq_eval_tcode (value tcode, value e) { diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index cc59558e1..041e0795d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -4,7 +4,7 @@ open Cbytecodes open Cemitcodes open Term open Declarations -open Environ +open Pre_env (*i Compilation des variables + calcul des variables libres *) @@ -191,7 +191,7 @@ let get_strcst = function let rec str_const c = match kind_of_term c with | Sort s -> Bstrconst (Const_sorts s) - | Cast(c,_) -> str_const c + | Cast(c,_,_) -> str_const c | App(f,args) -> begin match kind_of_term f with @@ -201,18 +201,18 @@ let rec str_const c = let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in if nparams + arity = Array.length args then - if arity = 0 then Bstrconst(Const_b0 num) - else - let rargs = Array.sub args nparams arity in - let b_args = Array.map str_const rargs in - try - let sc_args = Array.map get_strcst b_args in - Bstrconst(Const_bn(num, sc_args)) - with Not_found -> - Bmakeblock(num,b_args) + if arity = 0 then Bstrconst(Const_b0 num) + else + let rargs = Array.sub args nparams arity in + let b_args = Array.map str_const rargs in + try + let sc_args = Array.map get_strcst b_args in + Bstrconst(Const_bn(num, sc_args)) + with Not_found -> + Bmakeblock(num,b_args) else - let b_args = Array.map str_const args in - Bconstruct_app(num, nparams, arity, b_args) + let b_args = Array.map str_const args in + Bconstruct_app(num, nparams, arity, b_args) | _ -> Bconstr c end | Ind ind -> Bstrconst (Const_ind ind) @@ -274,7 +274,7 @@ let rec compile_constr reloc c sz cont = | Meta _ -> raise (Invalid_argument "Cbytegen.gen_lam : Meta") | Evar _ -> raise (Invalid_argument "Cbytegen.gen_lam : Evar") - | Cast(c,_) -> compile_constr reloc c sz cont + | Cast(c,_,_) -> compile_constr reloc c sz cont | Rel i -> pos_rel i reloc sz :: cont | Var id -> pos_named id reloc :: cont @@ -483,10 +483,6 @@ let compile_constant_body env body opaque boxed = else match kind_of_term body with | Const kn' -> BCallias (get_allias env kn') - | Construct _ -> - let res = compile env body in - let to_patch = to_memory res in - BCdefined (false, to_patch) | _ -> let res = compile env body in let to_patch = to_memory res in diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 135afb1e2..f761e4f60 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -3,7 +3,7 @@ open Cbytecodes open Cemitcodes open Term open Declarations -open Environ +open Pre_env diff --git a/kernel/closure.ml b/kernel/closure.ml index b79168785..625d3b0d0 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -357,22 +357,22 @@ let ref_value_cache info ref = let defined_vars flags env = (* if red_local_const (snd flags) then*) - fold_named_context - (fun env (id,b,t) e -> + Sign.fold_named_context + (fun (id,b,_) e -> match b with | None -> e | Some body -> (id, body)::e) - env ~init:[] + (named_context env) ~init:[] (* else []*) let defined_rels flags env = (* if red_local_const (snd flags) then*) - fold_rel_context - (fun env (id,b,t) (i,subs) -> + Sign.fold_rel_context + (fun (id,b,t) (i,subs) -> match b with | None -> (i+1, subs) | Some body -> (i+1, (i,body) :: subs)) - env ~init:(0,[]) + (rel_context env) ~init:(0,[]) (* else (0,[])*) @@ -512,7 +512,7 @@ type fconstr = { and fterm = | FRel of int | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * fconstr + | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | FInd of inductive | FConstruct of constructor @@ -603,10 +603,10 @@ let rec compact_constr (lg, subs as s) c k = | Evar(ev,v) -> let (v',s) = compact_vect s v k in if v==v' then c,s else mkEvar(ev,v'),s - | Cast(a,b) -> + | Cast(a,ck,b) -> let (a',s) = compact_constr s a k in let (b',s) = compact_constr s b k in - if a==a' && b==b' then c,s else mkCast(a',b'), s + if a==a' && b==b' then c,s else mkCast(a', ck, b'), s | App(f,v) -> let (f',s) = compact_constr s f k in let (v',s) = compact_vect s v k in @@ -693,9 +693,9 @@ let mk_clos_deep clos_fun env t = match kind_of_term t with | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> mk_clos env t - | Cast (a,b) -> + | Cast (a,k,b) -> { norm = Red; - term = FCast (clos_fun env a, clos_fun env b)} + term = FCast (clos_fun env a, k, clos_fun env b)} | App (f,v) -> { norm = Red; term = FApp (clos_fun env f, Array.map (clos_fun env) v) } @@ -728,8 +728,8 @@ let rec to_constr constr_fun lfts v = | FFlex (RelKey p) -> mkRel (reloc_rel p lfts) | FFlex (VarKey x) -> mkVar x | FAtom c -> exliftn lfts c - | FCast (a,b) -> - mkCast (constr_fun lfts a, constr_fun lfts b) + | FCast (a,k,b) -> + mkCast (constr_fun lfts a, k, constr_fun lfts b) | FFlex (ConstKey op) -> mkConst op | FInd op -> mkInd op | FConstruct op -> mkConstruct op @@ -976,7 +976,7 @@ let rec knh m stk = (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') | (None, stk') -> (m,stk')) - | FCast(t,_) -> knh t stk + | FCast(t,_,_) -> knh t stk (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> @@ -990,7 +990,7 @@ and knht e t stk = | Case(ci,p,t,br) -> knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) | Fix _ -> knh (mk_clos2 e t) stk - | Cast(a,b) -> knht e a stk + | Cast(a,_,_) -> knht e a stk | Rel n -> knh (clos_rel e n) stk | (Lambda _|Prod _|Construct _|CoFix _|Ind _| LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> diff --git a/kernel/closure.mli b/kernel/closure.mli index e394b15b8..4c0f9d32e 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -130,7 +130,7 @@ type fconstr type fterm = | FRel of int | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * fconstr + | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | FInd of inductive | FConstruct of constructor diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index f743970c6..fc2d09254 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -4,12 +4,9 @@ open Vm open Cemitcodes open Cbytecodes open Declarations -open Environ +open Pre_env open Cbytegen -open Cemitcodes - -open Format external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external free_tcode : tcode -> unit = "coq_static_free" @@ -78,6 +75,17 @@ let str_cst_tbl = Hashtbl.create 31 let annot_tbl = Hashtbl.create 31 (* (annot_switch * int) Hashtbl.t *) +(*************************************************************) +(*** Mise a jour des valeurs des variables et des constantes *) +(*************************************************************) + +exception NotEvaluated + +let key rk = + match !rk with + | Some k -> k + | _ -> raise NotEvaluated + (************************) (* traduction des patch *) @@ -98,55 +106,46 @@ let slot_for_annot key = Hashtbl.add annot_tbl key n; n -open Format - let rec slot_for_getglobal env kn = - let ck = lookup_constant_key kn env in - try constant_key_pos ck + let (cb,rk) = lookup_constant_key kn env in + try key rk with NotEvaluated -> - match force (constant_key_body ck).const_body_code with - | BCdefined(boxed,(code,pl,fv)) -> + let pos = + match Cemitcodes.force cb.const_body_code with + | BCdefined(boxed,(code,pl,fv)) -> let v = eval_to_patch env (code,pl,fv) in - let pos = - if boxed then set_global_boxed kn v - else set_global v in - set_pos_constant ck pos; - pos - | BCallias kn' -> - let pos = slot_for_getglobal env kn' in - set_pos_constant ck pos; - pos - | BCconstant -> - let v = val_of_constant kn in - let pos = set_global v in - set_pos_constant ck pos; - pos + if boxed then set_global_boxed kn v + else set_global v + | BCallias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant kn) in + rk := Some pos; + pos and slot_for_fv env fv= match fv with | FVnamed id -> - let nv = lookup_namedval id env in + let nv = lookup_named_val id env in begin - match kind_of_named nv with + match !nv with | VKvalue v -> v | VKaxiom id -> let v = val_of_named id in - set_namedval nv v; v - | VKdef(c,e) -> - let v = val_of_constr e c in - set_namedval nv v; v + nv := VKvalue v; v + | VKdef c -> + let v = val_of_constr (env_of_named id env) c in + nv := VKvalue v; v end | FVrel i -> - let rv = lookup_relval i env in + let rv = lookup_rel_val i env in begin - match kind_of_rel rv with + match !rv with | VKvalue v -> v | VKaxiom k -> let v = val_of_rel k in - set_relval rv v; v - | VKdef(c,e) -> - let v = val_of_constr e c in - set_relval rv v; v + rv := VKvalue v; v + | VKdef c -> + let v = val_of_constr (env_of_rel i env) c in + rv := VKvalue v; v end and eval_to_patch env (buff,pl,fv) = @@ -164,7 +163,7 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = try compile env c - with e -> print_string "can not compile \n";print_flush();raise e in + with e -> print_string "can not compile \n";Format.print_flush();raise e in eval_to_patch env (to_memory ccfv) let set_transparent_const kn = diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 4c56fc947..2640a4df1 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,6 +1,6 @@ open Names open Term -open Environ +open Pre_env val val_of_constr : env -> constr -> values diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9ce925207..82864bbe4 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -20,6 +20,9 @@ open Mod_subst (* This module defines the types of global declarations. This includes global constants/axioms and mutual inductive definitions *) +type engagement = ImpredicativeSet + + (*s Constants (internal representation) (Definition/Axiom) *) type constr_substituted = constr substituted @@ -191,3 +194,4 @@ and module_body = mod_type : module_type_body; mod_equiv : module_path option; mod_constraints : constraints } + diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 62a1cc07c..cdb394380 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -21,6 +21,9 @@ open Mod_subst declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types *) +type engagement = ImpredicativeSet + + (*s Constants (Definition/Axiom) *) type constr_substituted diff --git a/kernel/environ.ml b/kernel/environ.ml index 6d16632cd..45ae911a2 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -14,76 +14,31 @@ open Sign open Univ open Term open Declarations +open Pre_env +open Csymtable (* The type of environments. *) -type checksum = int +type named_context_val = Pre_env.named_context_val -type compilation_unit_name = dir_path * checksum +type env = Pre_env.env -type global = Constant | Inductive - -type key = int option ref -type constant_key = constant_body * key - -type engagement = ImpredicativeSet - -type globals = { - env_constants : constant_key Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body KNmap.t } - -type stratification = { - env_universes : universes; - env_engagement : engagement option -} - -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr * env - -and 'a lazy_val = 'a val_kind ref - -and env = { - env_globals : globals; - env_named_context : named_context; - env_named_val : (identifier * (identifier lazy_val)) list; - env_rel_context : rel_context; - env_rel_val : inv_rel_key lazy_val list; - env_nb_rel : int; - env_stratification : stratification } - -let empty_env = { - env_globals = { - env_constants = Cmap.empty; - env_inductives = KNmap.empty; - env_modules = MPmap.empty; - env_modtypes = KNmap.empty }; - env_named_context = empty_named_context; - env_named_val = []; - env_rel_context = empty_rel_context; - env_rel_val = []; - env_nb_rel = 0; - env_stratification = { - env_universes = initial_universes; - env_engagement = None } } +let pre_env env = env +let empty_named_context_val = empty_named_context_val +let empty_env = empty_env let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context +let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context let empty_context env = env.env_rel_context = empty_rel_context && env.env_named_context = empty_named_context -exception NotEvaluated -exception AllReadyEvaluated - (* Rel context *) let lookup_rel n env = Sign.lookup_rel n env.env_rel_context @@ -98,18 +53,7 @@ let evaluable_rel n env = let nb_rel env = env.env_nb_rel -let push_rel d env = - let _,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom env.env_nb_rel) - | Some c -> ref (VKdef(c,env)) - in - { env with - env_rel_context = add_rel_decl d env.env_rel_context; - env_rel_val = rval :: env.env_rel_val; - env_nb_rel = env.env_nb_rel + 1 } - +let push_rel = push_rel let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x @@ -126,105 +70,87 @@ let reset_rel_context env = env_nb_rel = 0 } let fold_rel_context f env ~init = - snd (Sign.fold_rel_context - (fun d (env,e) -> (push_rel d env, f env d e)) - (rel_context env) ~init:(reset_rel_context env,init)) - -(* Abstract machine rel values *) -type relval = int lazy_val - -let kind_of_rel r = !r - -let set_relval r v = - match !r with - | VKvalue _ -> raise AllReadyEvaluated - | _ -> r := VKvalue v - -let lookup_relval n env = - try List.nth env.env_rel_val (n - 1) - with _ -> raise Not_found - + let rec fold_right env = + match env.env_rel_context with + | [] -> init + | rd::rc -> + let env = + { env with + env_rel_context = rc; + env_rel_val = List.tl env.env_rel_val; + env_nb_rel = env.env_nb_rel - 1 } in + f env rd (fold_right env) + in fold_right env + (* Named context *) -let lookup_named id env = - Sign.lookup_named id env.env_named_context - + +let named_context_of_val = fst + +(* [map_named_val f ctxt] apply [f] to the body and the type of + each declarations. + *** /!\ *** [f t] should be convertible with t *) +let map_named_val f (ctxt,ctxtv) = + let ctxt = + List.map (fun (id,body,typ) -> (id, option_app f body, f typ)) ctxt in + (ctxt,ctxtv) + +let empty_named_context = empty_named_context + +let push_named = push_named +let push_named_context_val = push_named_context_val + +let val_of_named_context ctxt = + List.fold_right push_named_context_val ctxt empty_named_context_val + + +let lookup_named id env = Sign.lookup_named id env.env_named_context +let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt (* A local const is evaluable if it is defined *) + +let named_type id env = + let (_,_,t) = lookup_named id env in t + +let named_body id env = + let (_,b,_) = lookup_named id env in b + let evaluable_named id env = try - match lookup_named id env with - (_,Some _,_) -> true - | _ -> false - with Not_found -> - false + match named_body id env with + |Some _ -> true + | _ -> false + with Not_found -> false -let push_named d env = - let id,body,_ = d in - let rval = - match body with - | None -> ref (VKaxiom id) - | Some c -> ref (VKdef(c,env)) - - in - { env with - env_named_context = Sign.add_named_decl d env.env_named_context; - env_named_val = (id,rval):: env.env_named_val } - -let reset_context env = +let reset_with_named_context (ctxt,ctxtv) env = { env with - env_named_context = empty_named_context; - env_named_val = []; + env_named_context = ctxt; + env_named_vals = ctxtv; env_rel_context = empty_rel_context; env_rel_val = []; env_nb_rel = 0 } -let reset_with_named_context ctxt env = - Sign.fold_named_context push_named ctxt ~init:(reset_context env) - +let reset_context = reset_with_named_context empty_named_context_val + let fold_named_context f env ~init = - snd (Sign.fold_named_context - (fun d (env,e) -> (push_named d env, f env d e)) - (named_context env) ~init:(reset_context env,init)) - + let rec fold_right env = + match env.env_named_context with + | [] -> init + | d::ctxt -> + let env = + reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + f env d (fold_right env) + in fold_right env + let fold_named_context_reverse f ~init env = - Sign.fold_named_context_reverse f ~init:init (named_context env) - -(* Abstract machine values of local vars referred by names *) -type namedval = identifier lazy_val - -let kind_of_named r = !r - -let set_namedval r v = - match !r with - | VKvalue _ -> raise AllReadyEvaluated - | _ -> r := VKvalue v - -let lookup_namedval id env = - snd (List.find (fun (id',_) -> id = id') env.env_named_val) - + Sign.fold_named_context_reverse f ~init:init (named_context env) + (* Global constants *) -let notevaluated = None - -let constant_key_pos (cb,r) = - match !r with - | None -> raise NotEvaluated - | Some key -> key - -let constant_key_body = fst - -let set_pos_constant (cb,r) bpos = - if !r = notevaluated then r := Some bpos - else raise AllReadyEvaluated - -let lookup_constant_key kn env = - Cmap.find kn env.env_globals.env_constants - -let lookup_constant kn env = constant_key_body (lookup_constant_key kn env) +let lookup_constant = lookup_constant let add_constant kn cs env = let new_constants = - Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in + Cmap.add kn (cs,ref None) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in @@ -256,8 +182,7 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false (* Mutual Inductives *) -let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives +let lookup_mind = lookup_mind let add_mind kn mib env = let new_inds = KNmap.add kn mib env.env_globals.env_inductives in @@ -341,7 +266,6 @@ let keep_hyps env needed = (named_context env) ~init:empty_named_context - (* Modules *) let add_modtype ln mtb env = @@ -381,3 +305,61 @@ type unsafe_type_judgment = { utj_val : constr; utj_type : sorts } +(*s Compilation of global declaration *) + +let compile_constant_body = Cbytegen.compile_constant_body + +(*s Special functions for the refiner (logic.ml) *) + +let clear_hyps ids check (ctxt,vals) = + let ctxt,vals,rmv = + List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> + if List.mem id ids then (ctxt,vals,id::rmv) + else begin + check rmv d; + (d::ctxt,v::vals,rmv) + end) ctxt vals ([],[],[]) + in ((ctxt,vals),rmv) + +exception Hyp_not_found + +let rec apply_to_hyp (ctxt,vals) id f = + let rec aux rtail ctxt vals = + match ctxt, vals with + | (idc,c,ct as d)::ctxt, v::vals -> + if idc = id then + (f ctxt d rtail)::ctxt, v::vals + else + let ctxt',vals' = aux (d::rtail) ctxt vals in + d::ctxt', v::vals' + | [],[] -> raise Hyp_not_found + | _, _ -> assert false + in aux [] ctxt vals + +let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g = + let rec aux ctxt vals = + match ctxt,vals with + | (idc,c,ct as d)::ctxt, v::vals -> + if idc = id then + let sign = ctxt,vals in + push_named_context_val (f d sign) sign + else + let (ctxt,vals as sign) = aux ctxt vals in + push_named_context_val (g d sign) sign + | [],[] -> raise Hyp_not_found + | _,_ -> assert false + in aux ctxt vals + +let insert_after_hyp (ctxt,vals) id d check = + let rec aux ctxt vals = + match ctxt, vals with + | (idc,c,ct as d')::ctxt', v::vals' -> + if idc = id then begin + check ctxt; + push_named_context_val d (ctxt,vals) + end else + let ctxt,vals = aux ctxt vals in + d::ctxt, v::vals + | [],[] -> raise Hyp_not_found + | _, _ -> assert false + in aux ctxt vals diff --git a/kernel/environ.mli b/kernel/environ.mli index 20027d32a..b8f565e45 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -30,15 +30,20 @@ open Sign - a set of universe constraints - a flag telling if Set is, can be, or cannot be set impredicative *) + + + type env +val pre_env : env -> Pre_env.env + +type named_context_val val empty_env : env val universes : env -> Univ.universes val rel_context : env -> rel_context val named_context : env -> named_context - -type engagement = ImpredicativeSet +val named_context_val : env -> named_context_val val engagement : env -> engagement option @@ -47,6 +52,7 @@ val empty_context : env -> bool (************************************************************************) (*s Context of de Bruijn variables ([rel_context]) *) +val nb_rel : env -> int val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env @@ -56,39 +62,41 @@ val push_rec_types : rec_declaration -> env -> env val lookup_rel : int -> env -> rel_declaration val evaluable_rel : int -> env -> bool -(* Abstract machine rel values *) -type 'a val_kind = - | VKvalue of values - | VKaxiom of 'a - | VKdef of constr * env - -type relval - -val kind_of_rel : relval -> inv_rel_key val_kind -val set_relval : relval -> values -> unit -val lookup_relval : int -> env -> relval -val nb_rel : env -> int (*s Recurrence on [rel_context] *) val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a (************************************************************************) (* Context of variables (section variables and goal assumptions) *) + +val named_context_of_val : named_context_val -> named_context +val val_of_named_context : named_context -> named_context_val +val empty_named_context_val : named_context_val + + +(* [map_named_val f ctxt] apply [f] to the body and the type of + each declarations. + *** /!\ *** [f t] should be convertible with t *) +val map_named_val : + (constr -> constr) -> named_context_val -> named_context_val + val push_named : named_declaration -> env -> env +val push_named_context_val : + named_declaration -> named_context_val -> named_context_val + + (* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) -val lookup_named : variable -> env -> named_declaration -val evaluable_named : variable -> env -> bool -(* Abstract machine values of local vars referred by names *) -type namedval - -val kind_of_named : namedval -> identifier val_kind -val set_namedval : namedval -> values -> unit -val lookup_namedval : identifier -> env -> namedval +val lookup_named : variable -> env -> named_declaration +val lookup_named_val : variable -> named_context_val -> named_declaration +val evaluable_named : variable -> env -> bool +val named_type : variable -> env -> types +val named_body : variable -> env -> constr option (*s Recurrence on [named_context]: older declarations processed first *) + val fold_named_context : (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a @@ -99,7 +107,7 @@ val fold_named_context_reverse : (* This forgets named and rel contexts *) val reset_context : env -> env (* This forgets rel context and sets a new named context *) -val reset_with_named_context : named_context -> env -> env +val reset_with_named_context : named_context_val -> env -> env (************************************************************************) (*s Global constants *) @@ -108,15 +116,7 @@ val add_constant : constant -> constant_body -> env -> env (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) -type constant_key -exception NotEvaluated -exception AllReadyEvaluated -val constant_key_pos : constant_key -> int -val constant_key_body : constant_key -> constant_body -val set_pos_constant : constant_key -> int -> unit - -val lookup_constant_key : constant -> env -> constant_key val lookup_constant : constant -> env -> constant_body val evaluable_constant : constant -> env -> bool @@ -183,7 +183,35 @@ type unsafe_type_judgment = { utj_type : sorts } +(*s Compilation of global declaration *) + +val compile_constant_body : + env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code + (* opaque *) (* boxed *) + +(*s Functions for proofs/logic.ml *) +val clear_hyps : + variable list -> (variable list -> named_declaration -> unit) -> + named_context_val -> named_context_val * variable list + +exception Hyp_not_found +(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and + return [tail::(f head (id,_,_) (rev tail))::head]. + the value associated to id should not change *) +val apply_to_hyp : named_context_val -> variable -> + (named_context -> named_declaration -> named_context -> named_declaration) -> + named_context_val +(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into + [tail::(id,_,_)::head] and + return [(g tail)::(f (id,_,_))::head]. *) +val apply_to_hyp_and_dependent_on : named_context_val -> variable -> + (named_declaration -> named_context_val -> named_declaration) -> + (named_declaration -> named_context_val -> named_declaration) -> + named_context_val +val insert_after_hyp : named_context_val -> variable -> + named_declaration -> + (named_context -> unit) -> named_context_val diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 218d7f822..d12c3a213 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -132,7 +132,7 @@ let rec infos_and_sort env t = let logic = not (is_info_type env varj) in let small = Term.is_small varj.utj_type in (logic,small) :: (infos_and_sort env1 c2) - | Cast (c,_) -> infos_and_sort env c + | Cast (c,_,_) -> infos_and_sort env c | _ -> [] let small_unit constrsinfos = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b5d825e84..af237d1d1 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -630,7 +630,7 @@ let check_one_fix renv recpos def = (* The cases below simply check recursively the condition on the subterms *) - | Cast (a,b) -> + | Cast (a,_, b) -> List.for_all (check_rec_call renv) (a::b::l) | Lambda (x,a,b) -> diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index bb3027aa8..efbee6af2 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -97,7 +97,7 @@ and merge_with env mtb with_decl = SPBconst {cb with const_body = body; const_body_code = Cemitcodes.from_val - (Cbytegen.compile_constant_body env' body false false); + (compile_constant_body env' body false false); const_constraints = cst} | Some b -> let cst1 = Reduction.conv env' c (Declarations.force b) in @@ -106,7 +106,7 @@ and merge_with env mtb with_decl = SPBconst {cb with const_body = body; const_body_code = Cemitcodes.from_val - (Cbytegen.compile_constant_body env' body false false); + (compile_constant_body env' body false false); const_constraints = cst} end (* and what about msid's ????? Don't they clash ? *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 7b4c3095d..b20e7259d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -257,7 +257,7 @@ let strengthen_const env mp l cb = const_body = const_subs; const_opaque = false; const_body_code = Cemitcodes.from_val - (Cbytegen.compile_constant_body env const_subs false false) + (compile_constant_body env const_subs false false) } let strengthen_mind env mp l mib = match mib.mind_equiv with diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 156e3a44a..2467e941f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -342,31 +342,28 @@ let conv_leq_vecti env v1 v2 = (* option for conversion *) -let vm_fconv = ref fconv - -let set_default_vm_conv _ = vm_fconv := fconv -let set_vm_conv_cmp f = vm_fconv := f - +let vm_conv = ref fconv +let set_vm_conv f = vm_conv := f let vm_conv cv_pb env t1 t2 = try - !vm_fconv cv_pb env t1 t2 + !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) clos_fconv cv_pb env t1 t2 -let vm_conv_leq_vecti env v1 v2 = - array_fold_left2_i - (fun i c t1 t2 -> - let c' = - try vm_conv CUMUL env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i) in - Constraint.union c c') - Constraint.empty - v1 - v2 +let default_conv = ref fconv -let vm_conv_leq = vm_conv CUMUL +let set_default_conv f = default_conv := f + +let default_conv cv_pb env t1 t2 = + try + !default_conv cv_pb env t1 t2 + with Not_found | Invalid_argument _ -> + (* If compilation fails, fall-back to closure conversion *) + clos_fconv cv_pb env t1 t2 + +let default_conv_leq = default_conv CUMUL (* let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = @@ -419,7 +416,7 @@ let dest_prod_assum env = | LetIn (x,b,t,c) -> let d = (x,Some b,t) in prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c - | Cast (c,_) -> prodec_rec env l c + | Cast (c,_,_) -> prodec_rec env l c | _ -> l,rty in prodec_rec env Sign.empty_rel_context diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 5d383e61e..60cd999d8 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -44,12 +44,12 @@ val conv_leq : types conversion_function val conv_leq_vecti : types array conversion_function (* option for conversion *) - -val set_default_vm_conv : unit -> unit -val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit +val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val vm_conv_leq_vecti : types array conversion_function -val vm_conv_leq : types conversion_function + +val set_default_conv : (conv_pb -> types conversion_function) -> unit +val default_conv : conv_pb -> types conversion_function +val default_conv_leq : types conversion_function (************************************************************************) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 83aa3e943..5412287ee 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -67,7 +67,7 @@ val add_constraints : Univ.constraints -> safe_environment -> safe_environment (* Settin the strongly constructive or classical logical engagement *) -val set_engagement : Environ.engagement -> safe_environment -> safe_environment +val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) diff --git a/kernel/sign.ml b/kernel/sign.ml index a90b43335..dd22d5b8c 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -122,7 +122,7 @@ let destArity = match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly "destArity: not an arity" in @@ -134,7 +134,7 @@ let rec isArity c = match kind_of_term c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) - | Cast (c,_) -> isArity c + | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false @@ -145,7 +145,7 @@ let decompose_prod_assum = match kind_of_term c with | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec empty_rel_context @@ -157,7 +157,7 @@ let decompose_lam_assum = match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_) -> lamdec_rec l c + | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec empty_rel_context @@ -172,7 +172,7 @@ let decompose_prod_n_assum n = else match kind_of_term c with | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c - | Cast (c,_) -> prodec_rec l n c + | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in prodec_rec empty_rel_context n @@ -187,7 +187,7 @@ let decompose_lam_n_assum n = else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c - | Cast (c,_) -> lamdec_rec l n c + | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec empty_rel_context n diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5ab9f9a02..0c339e8b8 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -134,7 +134,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let rec names_prod_letin t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) - | Cast(t,_) -> names_prod_letin t + | Cast(t,_,_) -> names_prod_letin t | _ -> [] in assert (Array.length mib1.mind_packets = 1); diff --git a/kernel/term.ml b/kernel/term.ml index 8bd079ce5..f59ba5d66 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -21,6 +21,8 @@ open Esubst type existential_key = int type metavariable = int +(* This defines the strategy to use for verifiying a Cast *) + (* This defines Cases annotations *) type pattern_source = DefaultPat of int | RegularPat type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle @@ -56,6 +58,8 @@ let family_of_sort = function (* Constructions as implemented *) (********************************************************************) +type cast_kind = VMcast | DEFAULTcast + (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = existential_key * 'constr array @@ -74,7 +78,7 @@ type ('constr, 'types) kind_of_term = | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts - | Cast of 'constr * 'types + | Cast of 'constr * cast_kind * 'types | Prod of name * 'types * 'types | Lambda of name * 'types * 'constr | LetIn of name * 'constr * 'types * 'constr @@ -89,14 +93,14 @@ type ('constr, 'types) kind_of_term = (* Experimental *) type ('constr, 'types) kind_of_type = | SortType of sorts - | CastType of 'types * 'types + | CastType of 'types * 'types | ProdType of name * 'types * 'types | LetInType of name * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array let kind_of_type = function | Sort s -> SortType s - | Cast (c,t) -> CastType (c, t) + | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) | LetIn (na,b,t,c) -> LetInType (na, b, t, c) | App (c,l) -> AtomicType (c, l) @@ -123,7 +127,7 @@ let comp_term t1 t2 = | Meta m1, Meta m2 -> m1 == m2 | Var id1, Var id2 -> id1 == id2 | Sort s1, Sort s2 -> s1 == s2 - | Cast (c1,t1), Cast (c2,t2) -> c1 == c2 & t1 == t2 + | Cast (c1,_,t1), Cast (c2,_,t2) -> c1 == c2 & t1 == t2 | Prod (n1,t1,c1), Prod (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> @@ -154,7 +158,7 @@ let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t = | Meta x -> Meta x | Var x -> Var (sh_id x) | Sort s -> Sort (sh_sort s) - | Cast (c,t) -> Cast (sh_rec c, sh_rec t) + | Cast (c, k, t) -> Cast (sh_rec c, k, (sh_rec t)) | Prod (na,t,c) -> Prod (sh_na na, sh_rec t, sh_rec c) | Lambda (na,t,c) -> Lambda (sh_na na, sh_rec t, sh_rec c) | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c) @@ -207,11 +211,12 @@ let mkVar id = Var id let mkSort s = Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) *) -let mkCast (t1,t2) = +(* (that means t2 is declared as the type of t1) + [s] is the strategy to use when *) +let mkCast (t1,k2,t2) = match t1 with - | Cast (t,_) -> Cast (t,t2) - | _ -> Cast (t1,t2) + | Cast (c,k1, _) when k1 = k2 -> Cast (c,k1,t2) + | _ -> Cast (t1,k2,t2) (* Constructs the product (x:t1)t2 *) let mkProd (x,t1,t2) = Prod (x,t1,t2) @@ -310,22 +315,22 @@ let destSort c = match kind_of_term c with let rec isprop c = match kind_of_term c with | Sort (Prop _) -> true - | Cast (c,_) -> isprop c + | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind_of_term c with | Sort (Prop Null) -> true - | Cast (c,_) -> is_Prop c + | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind_of_term c with | Sort (Prop Pos) -> true - | Cast (c,_) -> is_Set c + | Cast (c,_,_) -> is_Set c | _ -> false let rec is_Type c = match kind_of_term c with | Sort (Type _) -> true - | Cast (c,_) -> is_Type c + | Cast (c,_,_) -> is_Type c | _ -> false let isType = function @@ -345,10 +350,11 @@ let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false (* Destructs a casted term *) let destCast c = match kind_of_term c with - | Cast (t1, t2) -> (t1,t2) + | Cast (t1,k,t2) -> (t1,k,t2) | _ -> invalid_arg "destCast" -let isCast c = match kind_of_term c with Cast (_,_) -> true | _ -> false +let isCast c = match kind_of_term c with Cast _ -> true | _ -> false + (* Tests if a de Bruijn index *) let isRel c = match kind_of_term c with Rel _ -> true | _ -> false @@ -434,7 +440,7 @@ let rec collapse_appl c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_) when isApp c -> collapse_rec c cl2 + | Cast (c,_,_) when isApp c -> collapse_rec c cl2 | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) in collapse_rec f cl @@ -450,11 +456,11 @@ let rec strip_head_cast c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_) -> collapse_rec c cl2 + | Cast (c,_,_) -> collapse_rec c cl2 | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) in collapse_rec f cl - | Cast (c,t) -> strip_head_cast c + | Cast (c,_,_) -> strip_head_cast c | _ -> c (****************************************************************************) @@ -468,7 +474,7 @@ let rec strip_head_cast c = match kind_of_term c with let fold_constr f acc c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc - | Cast (c,t) -> f (f acc c) t + | Cast (c,_,t) -> f (f acc c) t | Prod (_,t,c) -> f (f acc t) c | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c @@ -489,7 +495,7 @@ let fold_constr f acc c = match kind_of_term c with let iter_constr f c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () - | Cast (c,t) -> f c; f t + | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c @@ -508,7 +514,7 @@ let iter_constr f c = match kind_of_term c with let iter_constr_with_binders g f n c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () - | Cast (c,t) -> f n c; f n t + | Cast (c,_,t) -> f n c; f n t | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c @@ -529,7 +535,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with let map_constr f c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> mkCast (f c, f t) + | Cast (c,k,t) -> mkCast (f c, k, f t) | Prod (na,t,c) -> mkProd (na, f t, f c) | Lambda (na,t,c) -> mkLambda (na, f t, f c) | LetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) @@ -550,7 +556,7 @@ let map_constr f c = match kind_of_term c with let map_constr_with_binders g f l c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> mkCast (f l c, f l t) + | Cast (c,k,t) -> mkCast (f l c, k, f l t) | Prod (na,t,c) -> mkProd (na, f l t, f (g l) c) | Lambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c) @@ -575,8 +581,8 @@ let compare_constr f t1 t2 = | Meta m1, Meta m2 -> m1 = m2 | Var id1, Var id2 -> id1 = id2 | Sort s1, Sort s2 -> s1 = s2 - | Cast (c1,_), _ -> f c1 t2 - | _, Cast (c2,_) -> f t1 c2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 @@ -607,6 +613,8 @@ let compare_constr f t1 t2 = type types = constr +type strategy = types option + let type_app f tt = f tt let body_of_type ty = ty @@ -673,7 +681,7 @@ let noccur_with_meta n m term = | Rel p -> if n<=p & p<n+m then raise LocalOccur | App(f,cl) -> (match kind_of_term f with - | Cast (c,_) when isMeta c -> () + | Cast (c,_,_) when isMeta c -> () | Meta _ -> () | _ -> iter_constr_with_binders succ occur_rec n c) | Evar (_, _) -> () @@ -942,17 +950,17 @@ let implicit_sort = Type (make_univ(make_dirpath[id_of_string"implicit"],0)) let mkImplicit = mkSort implicit_sort let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_) -> strip_outer_cast c + | Cast (c,_,_) -> strip_outer_cast c | _ -> c (* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) let under_outer_cast f c = match kind_of_term c with - | Cast (b,t) -> mkCast (f b,f t) + | Cast (b,k,t) -> mkCast (f b, k, f t) | _ -> f c let rec under_casts f c = match kind_of_term c with - | Cast (c,t) -> mkCast (under_casts f c, t) + | Cast (c,k,t) -> mkCast (under_casts f c, k, t) | _ -> f c (***************************) @@ -1003,7 +1011,7 @@ let rec to_lambda n prod = else match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) - | Cast (c,_) -> to_lambda n c + | Cast (c,_,_) -> to_lambda n c | _ -> errorlabstrm "to_lambda" (mt ()) let rec to_prod n lam = @@ -1012,7 +1020,7 @@ let rec to_prod n lam = else match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) - | Cast (c,_) -> to_prod n c + | Cast (c,_,_) -> to_prod n c | _ -> errorlabstrm "to_prod" (mt ()) (* pseudo-reduction rule: @@ -1042,7 +1050,7 @@ let prod_applist t nL = List.fold_left prod_app t nL let decompose_prod = let rec prodec_rec l c = match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec [] @@ -1052,7 +1060,7 @@ let decompose_prod = let decompose_lam = let rec lamdec_rec l c = match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c - | Cast (c,_) -> lamdec_rec l c + | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec [] @@ -1065,7 +1073,7 @@ let decompose_prod_n n = if n=0 then l,c else match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c - | Cast (c,_) -> prodec_rec l n c + | Cast (c,_,_) -> prodec_rec l n c | _ -> error "decompose_prod_n: not enough products" in prodec_rec [] n @@ -1078,7 +1086,7 @@ let decompose_lam_n n = if n=0 then l,c else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c - | Cast (c,_) -> lamdec_rec l n c + | Cast (c,_,_) -> lamdec_rec l n c | _ -> error "decompose_lam_n: not enough abstractions" in lamdec_rec [] n @@ -1088,7 +1096,7 @@ let decompose_lam_n n = let nb_lam = let rec nbrec n c = match kind_of_term c with | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_) -> nbrec n c + | Cast (c,_,_) -> nbrec n c | _ -> n in nbrec 0 @@ -1097,7 +1105,7 @@ let nb_lam = let nb_prod = let rec nbrec n c = match kind_of_term c with | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_) -> nbrec n c + | Cast (c,_,_) -> nbrec n c | _ -> n in nbrec 0 diff --git a/kernel/term.mli b/kernel/term.mli index 9c8f2fa10..70388808a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -12,6 +12,7 @@ open Names (*i*) + (*s The sorts of CCI. *) type contents = Pos | Null @@ -99,9 +100,13 @@ val mkProp : types val mkSet : types val mkType : Univ.universe -> types + +(* This defines the strategy to use for verifiying a Cast *) +type cast_kind = VMcast | DEFAULTcast + (* Constructs the term [t1::t2], i.e. the term $t_1$ casted with the type $t_2$ (that means t2 is declared as the type of t1). *) -val mkCast : constr * types -> constr +val mkCast : constr * cast_kind * constr -> constr (* Constructs the product [(x:t1)t2] *) val mkProd : name * types * types -> types @@ -192,7 +197,7 @@ type ('constr, 'types) kind_of_term = | Meta of metavariable | Evar of 'constr pexistential | Sort of sorts - | Cast of 'constr * 'types + | Cast of 'constr * cast_kind * 'types | Prod of name * 'types * 'types | Lambda of name * 'types * 'constr | LetIn of name * 'constr * 'types * 'constr @@ -213,7 +218,7 @@ val kind_of_term : constr -> (constr, types) kind_of_term (* Experimental *) type ('constr, 'types) kind_of_type = | SortType of sorts - | CastType of 'types * 'types + | CastType of 'types * 'types | ProdType of name * 'types * 'types | LetInType of name * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array @@ -258,7 +263,7 @@ val destVar : constr -> identifier val destSort : constr -> sorts (* Destructs a casted term *) -val destCast : constr -> constr * types +val destCast : constr -> constr * cast_kind * constr (* Destructs the product $(x:t_1)t_2$ *) val destProd : types -> name * types * types diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b62e7b007..f76c5ffe3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -19,8 +19,6 @@ open Inductive open Environ open Entries open Type_errors -open Cemitcodes -open Cbytegen open Indtypes open Typeops @@ -28,13 +26,10 @@ let constrain_type env j cst1 = function | None -> j.uj_type, cst1 | Some t -> let (tj,cst2) = infer_type env t in - let cst3 = - try vm_conv_leq env j.uj_type tj.utj_val - with NotConvertible -> error_actual_type env j tj.utj_val in + let (_,cst3) = judge_of_cast env j DEFAULTcast tj in assert (t = tj.utj_val); t, Constraint.union (Constraint.union cst1 cst2) cst3 - let translate_local_def env (b,topt) = let (j,cst) = infer env b in let (typ,cst) = constrain_type env j cst topt in @@ -99,7 +94,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) = (global_vars_set env (Declarations.force b)) (global_vars_set env typ) in - let tps = from_val (compile_constant_body env body op boxed) in + let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in let hyps = keep_hyps env ids in { const_hyps = hyps; const_body = body; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a70d81e66..3a968545f 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -19,10 +19,20 @@ open Entries open Reduction open Inductive open Type_errors - -let conv = vm_conv CONV -let conv_leq = vm_conv CUMUL -let conv_leq_vecti = vm_conv_leq_vecti + +let conv = default_conv CONV +let conv_leq = default_conv CUMUL + +let conv_leq_vecti env v1 v2 = + array_fold_left2_i + (fun i c t1 t2 -> + let c' = + try default_conv CUMUL env t1 t2 + with NotConvertible -> raise (NotConvertibleVect i) in + Constraint.union c c') + Constraint.empty + v1 + v2 (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env j = @@ -89,7 +99,7 @@ let judge_of_relative env n = (* Type of variables *) let judge_of_variable env id = try - let (_,_,ty) = lookup_named id env in + let ty = named_type id env in make_judge (mkVar id) ty with Not_found -> error_unbound_var env id @@ -100,10 +110,9 @@ let judge_of_variable env id = variables of the current env *) (* TODO: check order? *) let rec check_hyps_inclusion env sign = - let env_sign = named_context env in Sign.fold_named_context (fun (id,_,ty1) () -> - let (_,_,ty2) = Sign.lookup_named id env_sign in + let ty2 = named_type id env in if not (eq_constr ty2 ty1) then error "types do not match") sign @@ -233,11 +242,14 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj tj = +let judge_of_cast env cj k tj = let expected_type = tj.utj_val in try - let cst = conv_leq env cj.uj_type expected_type in - { uj_val = mkCast (j_val cj, expected_type); + let cst = + match k with + | VMcast -> vm_conv CUMUL env cj.uj_type expected_type + | DEFAULTcast -> conv_leq env cj.uj_type expected_type in + { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type }, cst with NotConvertible -> @@ -279,11 +291,11 @@ let judge_of_constructor env cstr (* Case. *) -let check_branch_types env cj (lft,explft) = - try conv_leq_vecti env lft explft +let check_branch_types env cj (lfj,explft) = + try conv_leq_vecti env (Array.map j_type lfj) explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val i lft.(i) explft.(i) + error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i) | Invalid_argument _ -> error_number_branches env cj (Array.length explft) @@ -294,8 +306,7 @@ let judge_of_case env ci pj cj lfj = let _ = check_case_info env (fst indspec) ci in let (bty,rslty,univ) = type_case_branches env indspec pj cj.uj_val in - let lft = Array.map j_type lfj in - let univ' = check_branch_types env cj (lft,bty) in + let univ' = check_branch_types env cj (lfj,bty) in ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty }, @@ -316,9 +327,7 @@ let type_fixpoint env lna lar vdefj = let lt = Array.length vdefj in assert (Array.length lar = lt); try - conv_leq_vecti env - (Array.map (fun j -> body_of_type j.uj_type) vdefj) - (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> error_ill_typed_rec_body env i lna vdefj lar @@ -375,17 +384,17 @@ let rec execute env cstr cu = | LetIn (name,c1,c2,c3) -> let (j1,cu1) = execute env c1 cu in let (j2,cu2) = execute_type env c2 cu1 in - let (_,cu3) = univ_combinator cu2 (judge_of_cast env j1 j2) in + let (_,cu3) = + univ_combinator cu2 (judge_of_cast env j1 DEFAULTcast j2) in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in let (j',cu4) = execute env1 c3 cu3 in (judge_of_letin env name j1 j2 j', cu4) - | Cast (c,t) -> + | Cast (c,k, t) -> let (cj,cu1) = execute env c cu in let (tj,cu2) = execute_type env t cu1 in univ_combinator cu2 - (judge_of_cast env cj tj) - + (judge_of_cast env cj k tj) (* Inductive types *) | Ind ind -> (judge_of_inductive env ind, cu) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index a537d793e..ed90c393e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -69,8 +69,8 @@ val judge_of_letin : (*s Type of a cast. *) val judge_of_cast : - env -> unsafe_judgment -> unsafe_type_judgment - -> unsafe_judgment * constraints + env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> + unsafe_judgment * constraints (*s Inductive types. *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8a2ced1d2..921cd7128 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -6,11 +6,11 @@ open Conv_oracle open Reduction open Closure open Vm -open Csymtable +open Csymtable open Univ -open Cbytecodes - +let val_of_constr env c = + val_of_constr (pre_env env) c (* Test la structure des piles *) @@ -194,8 +194,8 @@ let rec conv_eq pb t1 t2 cu = | Var id1, Var id2 -> if id1 = id2 then cu else raise NotConvertible | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu - | Cast (c1,_), _ -> conv_eq pb c1 t2 cu - | _, Cast (c2,_) -> conv_eq pb t1 c2 cu + | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu + | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu | Prod (_,t1,c1), Prod (_,t2,c2) -> conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu) | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu @@ -244,12 +244,14 @@ let vconv pb env t1 t2 = cu in cu -let use_vm = ref true -let _ = Reduction.set_vm_conv_cmp vconv +let _ = Reduction.set_vm_conv vconv + +let use_vm = ref false + let set_use_vm b = use_vm := b; - if b then Reduction.set_vm_conv_cmp vconv - else Reduction.set_default_vm_conv () + if b then Reduction.set_default_conv vconv + else Reduction.set_default_conv Reduction.conv_cmp let use_vm _ = !use_vm @@ -540,8 +542,6 @@ and nf_cofix env cf = let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in mkCoFix (init,(name,cft,cfb)) - - let cbv_vm env c t = let transp = transp_values () in if not transp then set_transp_values true; diff --git a/lib/options.ml b/lib/options.ml index 17e8af182..38c6e91a1 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -108,11 +108,6 @@ let _ = at_exit dump_it (* Options for the virtual machine *) -let print_bytecodes = ref false -let set_print_bytecodes b = print_bytecodes := b -let print_bytecodes _ = !print_bytecodes - - let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b let boxed_definitions _ = !boxed_definitions diff --git a/lib/options.mli b/lib/options.mli index 6b28158c3..d415f93d0 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -63,10 +63,6 @@ val dump_string : string -> unit (* Options for the virtual machine *) - -val set_print_bytecodes : bool -> unit -val print_bytecodes : unit -> bool - val set_boxed_definitions : bool -> unit val boxed_definitions : unit -> bool diff --git a/library/declare.ml b/library/declare.ml index bb66d3f26..5359290be 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -355,8 +355,10 @@ let variable_kind id = pi3 (Idmap.find id !vartab) let clear_proofs sign = - List.map - (fun (id,c,t as d) -> if variable_opacity id then (id,None,t) else d) sign + List.fold_right + (fun (id,c,t as d) signv -> + let d = if variable_opacity id then (id,None,t) else d in + Environ.push_named_context_val d signv) sign Environ.empty_named_context_val (* Global references. *) diff --git a/library/declare.mli b/library/declare.mli index c141985be..317c27281 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -73,7 +73,7 @@ val variable_strength : variable -> strength val variable_kind : variable -> local_kind val find_section_variable : variable -> section_path val last_section_hyps : dir_path -> identifier list -val clear_proofs : named_context -> named_context +val clear_proofs : named_context -> Environ.named_context_val (*s Global references *) diff --git a/library/global.ml b/library/global.ml index b8bc364b0..d4ad97a8c 100644 --- a/library/global.ml +++ b/library/global.ml @@ -39,6 +39,7 @@ let _ = let universes () = universes (env()) let named_context () = named_context (env()) +let named_context_val () = named_context_val (env()) let push_named_assum a = let (cst,env) = push_named_assum a !global_env in @@ -134,7 +135,7 @@ let env_of_context hyps = open Libnames let type_of_reference env = function - | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t + | VarRef id -> Environ.named_type id env | ConstRef c -> Environ.constant_type env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in diff --git a/library/global.mli b/library/global.mli index ef8472d08..a6ed6f411 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,6 +32,7 @@ val env : unit -> Environ.env val env_is_empty : unit -> bool val universes : unit -> universes +val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Sign.named_context (*s Extending env with variables and local definitions *) @@ -51,7 +52,7 @@ val add_modtype : identifier -> module_type_entry -> kernel_name val add_constraints : constraints -> unit -val set_engagement : Environ.engagement -> unit +val set_engagement : engagement -> unit (*s Interactive modules and module types *) (* Both [start_*] functions take the [dir_path] argument to create a @@ -93,5 +94,5 @@ val import : compiled_library -> Digest.t -> module_path * environment and a given context. *) val type_of_global : Libnames.global_reference -> types -val env_of_context : Sign.named_context -> Environ.env +val env_of_context : Environ.named_context_val -> Environ.env diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 1acf41ec6..e0d877b66 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -217,7 +217,7 @@ let subst_constr_expr a loc subs = | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) | CApp (_,(p,a),l) -> CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l) - | CCast (_,a,b) -> CCast (loc,subst a,subst b) + | CCast (_,a,k,b) -> CCast (loc,subst a,k,subst b) | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l) | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) | CHole _ | CEvar _ | CPatVar _ | CSort _ diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1a509b1e1..722703c1f 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -63,7 +63,7 @@ let set_loc loc = function | CPatVar(_,v) -> CPatVar(loc,v) | CEvar(_,ev) -> CEvar(loc,ev) | CSort(_,s) -> CSort(loc,s) - | CCast(_,a,b) -> CCast(loc,a,b) + | CCast(_,a,k,b) -> CCast(loc,a,k,b) | CNotation(_,n,l) -> CNotation(loc,n,l) | CNumeral(_,i) -> CNumeral(loc,i) | CDelimiters(_,s,e) -> CDelimiters(loc,s,e) @@ -162,7 +162,8 @@ GEXTEND Gram *) | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ] | "9" RIGHTA - [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ] + [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> + CCast (loc, c1, Term.DEFAULTcast,c2) ] | "8" RIGHTA [ c1 = operconstr; "->"; c2 = operconstr LEVEL "8"-> CArrow (loc, c1, c2) ] | "1" RIGHTA @@ -303,7 +304,7 @@ GEXTEND Gram | -> [] ] ] ; opt_casted_constr: - [ [ c = constr; ":"; t = constr -> CCast (loc, c, t) + [ [ c = constr; ":"; t = constr -> CCast (loc, c, DEFAULTcast, t) | c = constr -> c ] ] ; vardecls: diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 0111dbaf8..d2df2e144 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -33,7 +33,7 @@ let _ = Lexer.add_token ("","!") let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, ty) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty) let mk_lam = function ([],c) -> c @@ -168,8 +168,8 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,c2) ] + [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -329,7 +329,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,t)) + LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t)) ] ] ; binder: diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index f482aa152..4f25354b6 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -122,6 +122,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ] ; END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 603abd73a..0b4fc25f1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -78,8 +78,8 @@ GEXTEND Gram ] ] ; constr_body: - [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t) - | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t) + [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,Term.DEFAULTcast,t) + | ":"; t = constr; ":="; c = constr -> CCast(loc,c,Term.DEFAULTcast,t) | ":="; c = constr -> c ] ] ; vernac_list_tail: @@ -162,7 +162,7 @@ GEXTEND Gram | -> evar_constr loc ] ] ; opt_casted_constr: - [ [ c = constr; ":"; t = constr -> CCast(loc,c,t) + [ [ c = constr; ":"; t = constr -> CCast(loc,c,Term.DEFAULTcast,t) | c = constr -> c ] ] ; vardecls: diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 6277a9ab3..70f28a278 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -173,7 +173,7 @@ GEXTEND Gram def_body: [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c,t) -> DefineBody (bl, red, c, Some t) + CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) @@ -272,7 +272,7 @@ GEXTEND Gram t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t)) | id = name; ":="; b = lconstr -> match b with - CCast(_,b,t) -> (false,DefExpr(id,b,Some t)) + CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; assum_list: diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 20506abcf..02b35a1d8 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -151,7 +151,7 @@ let rec interp_xml_constr = function let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - RCast (loc, interp_xml_term x1, interp_xml_type x2) + RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2) | XmlTag (loc,"SORT",al,[]) -> RSort (loc, get_xml_sort al) | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 37abe4063..c47ad04c3 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -315,7 +315,7 @@ let rec pr inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom - | CCast (_,a,b) -> + | CCast (_,a,_,b) -> hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast | CNotation (_,"( _ )",[t]) -> str"("++ pr (max_int,E) t ++ str")", latom diff --git a/parsing/printer.ml b/parsing/printer.ml index 0677f2699..355bf6c94 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -405,7 +405,7 @@ let pr_prim_rule_v7 = function str(if occur_meta c then "Refine " else "Exact ") ++ Constrextern.with_meta_as_hole print_constr c - | Convert_concl c -> + | Convert_concl (c,_) -> (str"Change " ++ print_constr c) | Convert_hyp (id,None,t) -> @@ -472,7 +472,7 @@ let pr_prim_rule_v8 = function str(if occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole print_constr8 c - | Convert_concl c -> + | Convert_concl (c,_) -> (str"change " ++ print_constr8 c) | Convert_hyp (id,None,t) -> diff --git a/parsing/search.ml b/parsing/search.ml index ec7db4889..82829337a 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -41,7 +41,7 @@ let rec head_const c = match kind_of_term c with | Prod (_,_,d) -> head_const d | LetIn (_,_,_,d) -> head_const d | App (f,_) -> head_const f - | Cast (d,_) -> head_const d + | Cast (d,_,_) -> head_const d | _ -> c (* General search, restricted to head constant if [only_head] *) diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 942bce798..6b5b35dd2 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -53,12 +53,13 @@ let thin_sign osign sign = try if Sign.lookup_named id osign = (id,c,ty) then sign else raise Different - with Not_found | Different -> add_named_decl d sign) - sign ~init:empty_named_context + with Not_found | Different -> Environ.push_named_context_val d sign) + sign ~init:Environ.empty_named_context_val let rec print_proof sigma osign pf = let {evar_hyps=hyps; evar_concl=cl; evar_body=body} = pf.goal in + let hyps = Environ.named_context_of_val hyps in let hyps' = thin_sign osign hyps in match pf.ref with | None -> @@ -78,6 +79,7 @@ let pr_change gl = let rec print_script nochange sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in + let sign = Environ.named_context_of_val sign in match pf.ref with | None -> (if nochange then @@ -124,10 +126,12 @@ let rec print_info_script sigma osign pf = (str "." ++ fnl ()) else (str";" ++ brk(1,3) ++ - print_info_script sigma sign pf1) + print_info_script sigma + (Environ.named_context_of_val sign) pf1) | _ -> (str"." ++ fnl () ++ prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl)) + (print_info_script sigma + (Environ.named_context_of_val sign)) spfl)) let format_print_info_script sigma osign pf = hov 0 (print_info_script sigma osign pf) diff --git a/parsing/termast.ml b/parsing/termast.ml index b4871598d..3d191d4a9 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -344,7 +344,7 @@ let rec ast_of_raw = function | RProp Pos -> ope("SET",[]) | RType _ -> ope("TYPE",[])) | RHole _ -> ope("ISEVAR",[]) - | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t]) + | RCast (_,c,_,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t]) | RDynamic (loc,d) -> Dynamic (loc,d) and ast_of_eqn (_,ids,pl,c) = diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 33a9272d0..8042bff54 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -186,7 +186,7 @@ let rec norm_head info env t stack = let nargs = Array.map (cbv_stack_term info TOP env) args in norm_head info env head (stack_app (Array.to_list nargs) stack) | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) - | Cast (ct,_) -> norm_head info env ct stack + | Cast (ct,_,_) -> norm_head info env ct stack (* constants, axioms * the first pattern is CRUCIAL, n=0 happens very often: diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index cc3725210..6c4dbf5ed 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -78,7 +78,7 @@ let clenv_environments evd bound c = let rec clrec (e,metas) n c = match n, kind_of_term c with | (Some 0, _) -> (e, List.rev metas, c) - | (n, Cast (c,_)) -> clrec (e,metas) n c + | (n, Cast (c,_,_)) -> clrec (e,metas) n c | (n, Prod (na,c1,c2)) -> let mv = new_meta () in let dep = dependent (mkRel 1) c2 in @@ -96,7 +96,7 @@ let clenv_environments_evars env evd bound c = let rec clrec (e,ts) n c = match n, kind_of_term c with | (Some 0, _) -> (e, List.rev ts, c) - | (n, Cast (c,_)) -> clrec (e,ts) n c + | (n, Cast (c,_,_)) -> clrec (e,ts) n c | (n, Prod (na,c1,c2)) -> let e',constr = Evarutil.new_evar e env c1 in let dep = dependent (mkRel 1) c2 in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8b6e476c7..19c5ca54b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -177,7 +177,7 @@ let lookup_name_as_renamed env t s = if id=s then (Some n) else lookup avoid' (add_name (Name id) env_names) (n+1) c' | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c')) - | Cast (c,_) -> lookup avoid env_names n c + | Cast (c,_,_) -> lookup avoid env_names n c | _ -> None in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t @@ -191,7 +191,7 @@ let lookup_index_as_renamed env t n = (match concrete_name true [] empty_names_context name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c') - | Cast (c,_) -> lookup n d c + | Cast (c,_,_) -> lookup n d c | _ -> None in lookup n 1 t @@ -345,8 +345,8 @@ let rec detype tenv avoid env t = RVar (dummy_loc, id)) | Sort (Prop c) -> RSort (dummy_loc,RProp c) | Sort (Type u) -> RSort (dummy_loc,RType (Some u)) - | Cast (c1,c2) -> - RCast(dummy_loc,detype tenv avoid env c1, + | Cast (c1,k,c2) -> + RCast(dummy_loc,detype tenv avoid env c1, k, detype tenv avoid env c2) | Prod (na,ty,c) -> detype_binder tenv BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder tenv BLambda avoid env na ty c @@ -468,7 +468,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch = let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b - | Cast (c,_) -> (* Oui, il y a parfois des cast *) + | Cast (c,_,_) -> (* Oui, il y a parfois des cast *) buildrec ids patlist avoid env n c | _ -> (* eta-expansion : n'arrivera plus lorsque tous les @@ -600,10 +600,10 @@ let rec subst_raw subst raw = | RHole (loc, (BinderType _ | QuestionMark | CasesType | InternalHole | TomatchTypeParameter _)) -> raw - | RCast (loc,r1,r2) -> + | RCast (loc,r1,k,r2) -> let r1' = subst_raw subst r1 and r2' = subst_raw subst r2 in if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1',r2') + RCast (loc,r1',k,r2') | RDynamic _ -> raw diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a0c605857..aec4c2fa3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -339,9 +339,9 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with - | Cast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 + | Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 - | _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) + | _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) | Sort s1, Sort s2 when l1=[] & l2=[] -> (isevars,base_sort_cmp pbty s1 s2) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 12559d1da..4f956ffc6 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -48,7 +48,7 @@ let whd_castappevar_stack sigma c = match kind_of_term c with | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> whrec (existential_value sigma (ev,args), l) - | Cast (c,_) -> whrec (c, l) + | Cast (c,_,_) -> whrec (c, l) | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) | _ -> s in @@ -64,11 +64,7 @@ let tj_nf_evar = Pretype_errors.tj_nf_evar let nf_evar_info evc info = { evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = List.map - (fun (id,body,typ) -> - (id, - option_app (Reductionops.nf_evar evc) body, - Reductionops.nf_evar evc typ)) info.evar_hyps; + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; evar_body = info.evar_body} (**********************) @@ -107,7 +103,7 @@ let evars_to_metas sigma (emap, c) = let change_exist evar = let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in let n = new_meta() in - mkCast (mkMeta n, ty) in + mkCast (mkMeta n, DEFAULTcast, ty) in let rec replace c = match kind_of_term c with Evar (k,_ as ev) when Evd.in_dom emap' k -> change_exist ev @@ -163,8 +159,9 @@ let new_untyped_evar = (* All ids of sign must be distincts! *) let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance = - assert (List.length instance = named_context_length sign); - if not (list_distinct (ids_of_named_context sign)) then + let ctxt = named_context_of_val sign in + assert (List.length instance = named_context_length ctxt); + if not (list_distinct (ids_of_named_context ctxt)) then anomaly "new_evar_instance: two vars have the same name"; let newev = new_untyped_evar() in (evar_declare sign newev typ ~src:src evd, @@ -194,19 +191,18 @@ let make_subst env args = (* Converting the env into the sign of the evar to define *) let push_rel_context_to_named_context env = - let sign0 = named_context env in - let (subst,_,sign) = + let (subst,_,env) = Sign.fold_rel_context - (fun (na,c,t) (subst,avoid,sign) -> + (fun (na,c,t) (subst,avoid,env) -> let na = if na = Anonymous then Name(id_of_string"_") else na in let id = next_name_away na avoid in ((mkVar id)::subst, id::avoid, - add_named_decl (id,option_app (substl subst) c, + push_named (id,option_app (substl subst) c, type_app (substl subst) t) - sign)) - (rel_context env) ~init:([],ids_of_named_context sign0,sign0) - in (subst, sign) + env)) + (rel_context env) ~init:([],ids_of_named_context (named_context env),env) + in (subst, (named_context_val env)) let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ = let subst,sign = push_rel_context_to_named_context env in @@ -271,7 +267,7 @@ let inverse_instance env isevars ev evi inst rhs = if rigid then error() else if not strict_inverse && - List.exists (fun (id',_,_) -> id=id') evi.evar_hyps + List.exists (fun (id',_,_) -> id=id') (evar_context evi) then failwith "cannot solve pb yet" else t) @@ -308,13 +304,14 @@ let do_restrict_hyps evd ev args = let args = Array.to_list args in let evi = Evd.map (evars_of !evd) ev in let env = evar_env evi in - let hyps = evi.evar_hyps in + let hyps = evar_context evi in let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in (* No care is taken in case the evar type uses vars filtered out! Is it important ? *) let nc = - e_new_evar evd (reset_with_named_context sign env) - ~src:(evar_source ev !evd) evi.evar_concl in + let env = + Sign.fold_named_context push_named sign ~init:(reset_context env) in + e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) @@ -351,7 +348,8 @@ let real_clean env isevars ev evi args rhs = (try List.assoc t subst with Not_found -> if - not rigid or List.exists (fun (id',_,_) -> id=id') evi.evar_hyps + not rigid + or List.exists (fun (id',_,_) -> id=id') (evar_context evi) then t else error_not_clean env (evars_of !evd) ev rhs @@ -430,7 +428,7 @@ let head_is_evar isevars = let rec hrec k = match kind_of_term k with | Evar n -> not (Evd.is_defined_evar isevars n) | App (f,_) -> hrec f - | Cast (c,_) -> hrec c + | Cast (c,_,_) -> hrec c | _ -> false in hrec @@ -438,7 +436,7 @@ let head_is_evar isevars = let rec is_eliminator c = match kind_of_term c with | App _ -> true | Case _ -> true - | Cast (c,_) -> is_eliminator c + | Cast (c,_,_) -> is_eliminator c | _ -> false let head_is_embedded_evar isevars c = @@ -449,7 +447,7 @@ let head_evar = | Evar (ev,_) -> ev | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c - | Cast (c,_) -> hrec c + | Cast (c,_,_) -> hrec c | _ -> failwith "headconstant" in hrec @@ -494,7 +492,7 @@ let status_changed lev (pbty,t1,t2) = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else let evd = Evd.map (evars_of isevars) ev in - let hyps = evd.evar_hyps in + let hyps = evar_context evd in let (isevars',_,rsign) = array_fold_left2 (fun (isevars,sgn,rsgn) a1 a2 -> @@ -507,8 +505,9 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = in let nsign = List.rev rsign in let (evd',newev) = - new_evar isevars (reset_with_named_context nsign env) - ~src:(evar_source ev isevars) evd.evar_concl in + let env = + Sign.fold_named_context push_named nsign ~init:(reset_context env) in + new_evar isevars env ~src:(evar_source ev isevars) evd.evar_concl in let evd'' = Evd.evar_define ev newev evd' in evd'', [ev] @@ -585,7 +584,8 @@ let define_evar_as_arrow evd (ev,args) = let evenv = evar_env evi in let (evd1,dom) = new_evar evd evenv (new_Type()) in let nvar = - next_ident_away (id_of_string "x") (ids_of_named_context evi.evar_hyps) in + next_ident_away (id_of_string "x") + (ids_of_named_context (evar_context evi)) in let newenv = push_named (nvar, None, dom) evenv in let (evd2,rng) = new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index b3e5a4dd9..e6bdcbd9b 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -43,8 +43,8 @@ val e_new_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context -> evar_defs -> types -> ?src:loc * hole_kind -> constr list -> - evar_defs * constr + named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> + constr list -> evar_defs * constr (***********************************************************) (* Instanciate evars *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 35012f6bd..c58d921eb 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -29,9 +29,11 @@ type evar_body = type evar_info = { evar_concl : constr; - evar_hyps : named_context; + evar_hyps : named_context_val; evar_body : evar_body} +let evar_context evi = named_context_of_val evi.evar_hyps + module Evarmap = Intmap type evar_map1 = evar_info Evarmap.t @@ -107,14 +109,14 @@ let existential_type sigma (n,args) = try map sigma n with Not_found -> anomaly ("Evar "^(string_of_existential n)^" was not declared") in - let hyps = info.evar_hyps in + let hyps = evar_context info in instantiate_evar hyps info.evar_concl (Array.to_list args) exception NotInstantiatedEvar let existential_value sigma (n,args) = let info = map sigma n in - let hyps = info.evar_hyps in + let hyps = evar_context info in match evar_body info with | Evar_defined c -> instantiate_evar hyps c (Array.to_list args) @@ -519,7 +521,7 @@ let pr_meta_map mmap = let pr_idl idl = prlist_with_sep pr_spc pr_id idl let pr_evar_info evi = - let phyps = pr_idl (List.rev (ids_of_named_context evi.evar_hyps)) in + let phyps = pr_idl (List.rev (ids_of_named_context (evar_context evi))) in let pty = print_constr evi.evar_concl in let pb = match evi.evar_body with diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9dd0c33fb..506ce4487 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -31,9 +31,10 @@ type evar_body = type evar_info = { evar_concl : constr; - evar_hyps : named_context; + evar_hyps : Environ.named_context_val; evar_body : evar_body} +val evar_context : evar_info -> named_context type evar_map val empty : evar_map @@ -125,7 +126,7 @@ type hole_kind = val is_defined_evar : evar_defs -> existential -> bool val is_undefined_evar : evar_defs -> constr -> bool val evar_declare : - named_context -> evar -> types -> ?src:loc * hole_kind -> + Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind -> evar_defs -> evar_defs val evar_define : evar -> constr -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 8cd3dc2c4..0325a3acd 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -447,7 +447,7 @@ let make_case_gen env = make_case_com None env let change_sort_arity sort = let rec drec a = match kind_of_term a with - | Cast (c,t) -> drec c + | Cast (c,_,_) -> drec c | Prod (n,t,c) -> mkProd (n, t, drec c) | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c) | Sort _ -> mkSort sort diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d0dca036e..813a6a269 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -363,7 +363,7 @@ let control_only_guard env = | Case(_,p,c,b) -> control_rec p;control_rec c;Array.iter control_rec b | Evar (_,cl) -> Array.iter control_rec cl | App (c,cl) -> control_rec c; Array.iter control_rec cl - | Cast (c1,c2) -> control_rec c1; control_rec c2 + | Cast (c1,_, c2) -> control_rec c1; control_rec c2 | Prod (_,c1,c2) -> control_rec c1; control_rec c2 | Lambda (_,c1,c2) -> control_rec c1; control_rec c2 | LetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3 diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 34eb6d78d..64b63548d 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -179,15 +179,15 @@ let special_meta = (-1) (* Tries to match a subterm of [c] with [pat] *) let rec sub_match nocc pat c = match kind_of_term c with - | Cast (c1,c2) -> + | Cast (c1,k,c2) -> (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1] in - (lm,mkCast (List.hd lc, c2)) + (lm,mkCast (List.hd lc, k,c2)) | NextOccurrence nocc -> let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in - (lm,mkCast (List.hd lc, c2))) - | Lambda (x,c1,c2) -> + (lm,mkCast (List.hd lc, k,c2))) + | Lambda (x,c1,c2) -> (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with | PatternMatchingFailure -> let (lm,lc) = try_sub_match nocc pat [c1;c2] in diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index c67917477..df9139db1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -99,7 +99,7 @@ let rec pattern_of_constr t = | Var id -> PVar id | Sort (Prop c) -> PSort (RProp c) | Sort (Type _) -> PSort (RType None) - | Cast (c,_) -> pattern_of_constr c + | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) @@ -213,7 +213,7 @@ let rec pat_of_raw metas vars = function PSort s | RHole _ -> PMeta None - | RCast (_,c,t) -> + | RCast (_,c,_,t) -> Options.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d3a602ac2..f1f95695d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -53,7 +53,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=type_app (nf_evar sigma) v;utj_type=t} let env_ise sigma env = - let sign = named_context env in + let sign = named_context_val env in let ctxt = rel_context env in let env0 = reset_with_named_context sign env in Sign.fold_rel_context diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 148be3991..c0e20c399 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -262,7 +262,7 @@ let rec pretype tycon env isevars lvar = function | REvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = (Evd.map (evars_of !isevars) ev).evar_hyps in + let hyps = evar_context (Evd.map (evars_of !isevars) ev) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in @@ -637,7 +637,7 @@ let rec pretype tycon env isevars lvar = function let pat,new_avoid,new_ids = make_pat x avoid b ids in buildrec new_ids (pat::patlist) new_avoid (n-1) b - | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) + | RCast (_,c,_,_) -> (* Oui, il y a parfois des cast *) buildrec ids patlist avoid n c | _ -> (* eta-expansion *) @@ -873,7 +873,7 @@ let rec pretype tycon env isevars lvar = function let pat,new_avoid,new_ids = make_pat x avoid b ids in buildrec new_ids (pat::patlist) new_avoid (n-1) b - | RCast (_,c,_) -> (* Oui, il y a parfois des cast *) + | RCast (_,c,_,_) -> (* Oui, il y a parfois des cast *) buildrec ids patlist avoid n c | _ -> (* eta-expansion *) @@ -906,12 +906,12 @@ let rec pretype tycon env isevars lvar = function ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,t) -> + | RCast(loc,c,k,t) -> let tj = pretype_type empty_tycon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) (* ... except for Correctness *) - let v = mkCast (cj.uj_val, tj.utj_val) in + let v = mkCast (cj.uj_val, k, tj.utj_val) in let cj = { uj_val = v; uj_type = tj.utj_val } in inh_conv_coerce_to_tycon loc env isevars cj tycon @@ -1006,7 +1006,8 @@ let ise_infer_gen fail_evar sigma env lvar exptyp c = let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in let isevars = ref (create_evar_defs sigma) in let j = unsafe_infer tycon isevars env lvar c in - if fail_evar then check_evars env sigma isevars (mkCast(j.uj_val,j.uj_type)); + if fail_evar then + check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); (!isevars, j) let ise_infer_type_gen fail_evar sigma env lvar c = diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index b91531395..dde8490d0 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -70,7 +70,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * rawconstr + | RCast of loc * rawconstr * cast_kind * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr @@ -110,7 +110,7 @@ let map_rawconstr f = function | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) - | RCast (loc,c,t) -> RCast (loc,f c,f t) + | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x @@ -184,7 +184,7 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,t) -> (occur c) or (occur t) + | RCast (loc,c,_,t) -> (occur c) or (occur t) | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -211,7 +211,7 @@ let loc_of_rawconstr = function | RRec (loc,_,_,_,_,_) -> loc | RSort (loc,_) -> loc | RHole (loc,_) -> loc - | RCast (loc,_,_) -> loc + | RCast (loc,_,_,_) -> loc | RDynamic (loc,_) -> loc type 'a raw_red_flag = { diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index b56e862ac..4e4df6b39 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -67,7 +67,7 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * rawconstr + | RCast of loc * rawconstr * cast_kind * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 67c0fc856..c9ab57d02 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -47,7 +47,7 @@ type local_state_reduction_function = state -> state let rec whd_state (x, stack as s) = match kind_of_term x with | App (f,cl) -> whd_state (f, append_stack cl stack) - | Cast (c,_) -> whd_state (c, stack) + | Cast (c,_,_) -> whd_state (c, stack) | _ -> s let appterm_of_stack (f,s) = (f,list_of_stack s) @@ -254,7 +254,7 @@ let rec whd_state_gen flags env sigma = | Some body -> whrec (body, stack) | None -> s) | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack - | Cast (c,_) -> whrec (c, stack) + | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, append_stack cl stack) | Lambda (na,t,c) -> (match decomp_stack stack with @@ -299,7 +299,7 @@ let local_whd_state_gen flags = let rec whrec (x, stack as s) = match kind_of_term x with | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack - | Cast (c,_) -> whrec (c, stack) + | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, append_stack cl stack) | Lambda (_,_,c) -> (match decomp_stack stack with @@ -338,6 +338,47 @@ let local_whd_state_gen flags = in whrec +let rec whd_betaiotaevar_preserving_vm_cast env sigma t = + let rec stacklam_var subst t stack = + match (decomp_stack stack,kind_of_term t) with + | Some (h,stacktl), Lambda (_,_,c) -> + begin match kind_of_term h with + | Rel i when not (evaluable_rel i env) -> + stacklam_var (h::subst) c stacktl + | Var id when not (evaluable_named id env)-> + stacklam_var (h::subst) c stacktl + | _ -> whrec (substl subst t, stack) + end + | _ -> whrec (substl subst t, stack) + and whrec (x, stack as s) = + match kind_of_term x with + | Evar ev -> + (match existential_opt_value sigma ev with + | Some body -> whrec (body, stack) + | None -> s) + | Cast (c,VMcast,t) -> + let c = app_stack (whrec (c,empty_stack)) in + let t = app_stack (whrec (t,empty_stack)) in + (mkCast(c,VMcast,t),stack) + | Cast (c,DEFAULTcast,_) -> + whrec (c, stack) + | App (f,cl) -> whrec (f, append_stack cl stack) + | Lambda (na,t,c) -> + (match decomp_stack stack with + | Some (a,m) -> stacklam_var [a] c m + | _ -> s) + | Case (ci,p,d,lf) -> + let (c,cargs) = whrec (d, empty_stack) in + if reducible_mind_case c then + whrec (reduce_mind_case + {mP=p; mconstr=c; mcargs=list_of_stack cargs; + mci=ci; mlf=lf}, stack) + else + (mkCase (ci, p, app_stack (c,cargs), lf), stack) + | x -> s + in + app_stack (whrec (t,empty_stack)) + (* 1. Beta Reduction Functions *) let whd_beta_state = local_whd_state_gen beta @@ -512,22 +553,22 @@ let plain_instance s c = let rec irec u = match kind_of_term u with | Meta p -> (try List.assoc p s with Not_found -> u) | App (f,l) when isCast f -> - let (f,t) = destCast f in + let (f,_,t) = destCast f in let l' = Array.map irec l in (match kind_of_term f with - | Meta p -> - (* Don't flatten application nodes: this is used to extract a - proof-term from a proof-tree and we want to keep the structure - of the proof-tree *) - (try let g = List.assoc p s in - match kind_of_term g with - | App _ -> - let h = id_of_string "H" in - mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l')) - | _ -> mkApp (g,l') - with Not_found -> mkApp (f,l')) - | _ -> mkApp (irec f,l')) - | Cast (m,_) when isMeta m -> + | Meta p -> + (* Don't flatten application nodes: this is used to extract a + proof-term from a proof-tree and we want to keep the structure + of the proof-tree *) + (try let g = List.assoc p s in + match kind_of_term g with + | App _ -> + let h = id_of_string "H" in + mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l')) + | _ -> mkApp (g,l') + with Not_found -> mkApp (f,l')) + | _ -> mkApp (irec f,l')) + | Cast (m,_,_) when isMeta m -> (try List.assoc (destMeta m) s with Not_found -> u) | _ -> map_constr irec u in @@ -598,7 +639,7 @@ let splay_prod_assum env sigma = | LetIn (x,b,t,c) -> prodec_rec (push_rel (x, Some b, t) env) (Sign.add_rel_decl (x, Some b, t) l) c - | Cast (c,_) -> prodec_rec env l c + | Cast (c,_,_) -> prodec_rec env l c | _ -> l,t in prodec_rec env Sign.empty_rel_context diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 29a28f0f7..42a53224a 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -111,6 +111,10 @@ val whd_betadeltaiotaeta_stack : stack_reduction_function val whd_betadeltaiotaeta_state : state_reduction_function val whd_betadeltaiotaeta : reduction_function +val whd_betaiotaevar_preserving_vm_cast : reduction_function + + + val beta_applist : constr * constr list -> constr val hnf_prod_app : env -> evar_map -> constr -> constr -> constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a75e48a8e..715f54731 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -81,12 +81,12 @@ let typeur sigma metamap = | App(f,args)-> strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) - | Cast (c,t) -> t + | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) and sort_of env t = match kind_of_term t with - | Cast (c,s) when isSort s -> destSort s + | Cast (c,_, s) when isSort s -> destSort s | Sort (Prop c) -> type_0 | Sort (Type u) -> Type (Univ.super u) | Prod (name,t,c2) -> @@ -104,7 +104,7 @@ let typeur sigma metamap = and sort_family_of env t = match kind_of_term t with - | Cast (c,s) when isSort s -> family_of_sort (destSort s) + | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) | Sort (Prop c) -> InType | Sort (Type u) -> InType | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2 diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c9189ad2f..ef0867f7c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -440,7 +440,7 @@ let rec red_elim_const env sigma ref largs = and construct_const env sigma = let rec hnfstack (x, stack as s) = match kind_of_term x with - | Cast (c,_) -> hnfstack (c, stack) + | Cast (c,_,_) -> hnfstack (c, stack) | App (f,cl) -> hnfstack (f, append_stack cl stack) | Lambda (id,t,c) -> (match decomp_stack stack with @@ -494,7 +494,7 @@ let try_red_product env sigma c = let stack' = stack_assign stack recargnum recarg' in simpfun (app_stack (f,stack'))) | _ -> simpfun (appvect (redrec env f, l))) - | Cast (c,_) -> redrec env c + | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> mkProd (x, a, redrec (push_rel (x,None,a) env) b) | LetIn (x,a,b,t) -> redrec env (subst1 a t) | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) @@ -522,7 +522,7 @@ let hnf_constr env sigma c = stacklam redrec [a] c rest) | LetIn (n,b,t,c) -> stacklam redrec [b] c largs | App (f,cl) -> redrec (f, append_stack cl largs) - | Cast (c,_) -> redrec (c, largs) + | Cast (c,_,_) -> redrec (c, largs) | Case (ci,p,c,lf) -> (try redrec @@ -563,7 +563,7 @@ let whd_nf env sigma c = stacklam nf_app [a1] c2 rest) | LetIn (n,b,t,c) -> stacklam nf_app [b] c stack | App (f,cl) -> nf_app (f, append_stack cl stack) - | Cast (c,_) -> nf_app (c, stack) + | Cast (c,_,_) -> nf_app (c, stack) | Case (ci,p,d,lf) -> (try nf_app (special_red_case sigma env nf_app (ci,p,d,lf), stack) @@ -705,13 +705,13 @@ let rec substlin env name n ol c = let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) in (n3,ol3,mkCase (ci, p', d', Array.of_list lf')))) - | Cast (c1,c2) -> + | Cast (c1,k,c2) -> let (n1,ol1,c1') = substlin env name n ol c1 in (match ol1 with - | [] -> (n1,[],mkCast (c1',c2)) - | _ -> - let (n2,ol2,c2') = substlin env name n1 ol1 c2 in - (n2,ol2,mkCast (c1',c2'))) + | [] -> (n1,[],mkCast (c1',k,c2)) + | _ -> + let (n2,ol2,c2') = substlin env name n1 ol1 c2 in + (n2,ol2,mkCast (c1',k,c2'))) | Fix _ -> (warning "do not consider occurrences inside fixpoints"; (n,ol,c)) @@ -815,7 +815,7 @@ let one_step_reduce env sigma c = (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with | Reduced s' -> s' | NotReducible -> raise NotStepReducible) - | Cast (c,_) -> redrec (c,largs) + | Cast (c,_,_) -> redrec (c,largs) | _ when isEvalRef env x -> let ref = try destEvalRef x diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 1a6521d98..6db5d428a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -42,7 +42,7 @@ let rec pr_constr c = match kind_of_term c with | Meta n -> str "Meta(" ++ int n ++ str ")" | Var id -> pr_id id | Sort s -> print_sort s - | Cast (c,t) -> hov 1 + | Cast (c,_, t) -> hov 1 (str"(" ++ pr_constr c ++ cut() ++ str":" ++ pr_constr t ++ str")") | Prod (Name(id),t,c) -> hov 1 @@ -120,7 +120,8 @@ let pr_rel_decl env (na,c,typ) = let print_named_context env = hv 0 (fold_named_context - (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) + (fun env d pps -> + pps ++ ws 2 ++ pr_var_decl env d) env ~init:(mt ())) let print_rel_context env = @@ -132,7 +133,8 @@ let print_env env = let sign_env = fold_named_context (fun env d pps -> - let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt)) + let pidt = pr_var_decl env d in + (pps ++ fnl () ++ pidt)) env ~init:(mt ()) in let db_env = @@ -262,11 +264,11 @@ let rec strip_head_cast c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_) -> collapse_rec c cl2 + | Cast (c,_,_) -> collapse_rec c cl2 | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) in collapse_rec f cl - | Cast (c,t) -> strip_head_cast c + | Cast (c,_,_) -> strip_head_cast c | _ -> c (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate @@ -278,7 +280,7 @@ let rec strip_head_cast c = match kind_of_term c with let map_constr_with_named_binders g f l c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> mkCast (f l c, f l t) + | Cast (c,k,t) -> mkCast (f l c, k, f l t) | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c) | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) @@ -313,7 +315,7 @@ let fold_rec_types g (lna,typarray,_) e = let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,t) -> let c' = f l c in mkCast (c', f l t) + | Cast (c,k,t) -> let c' = f l c in mkCast (c',k,f l t) | Prod (na,t,c) -> let t' = f l t in mkProd (na, t', f (g (na,None,t) l) c) @@ -348,10 +350,10 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> cstr - | Cast (c,t) -> + | Cast (c,k, t) -> let c' = f l c in let t' = f l t in - if c==c' && t==t' then cstr else mkCast (c', t') + if c==c' && t==t' then cstr else mkCast (c', k, t') | Prod (na,t,c) -> let t' = f l t in let c' = f (g (na,None,t) l) c in @@ -405,7 +407,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with let fold_constr_with_binders g f n acc c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc - | Cast (c,t) -> f n (f n acc c) t + | Cast (c,_, t) -> f n (f n acc c) t | Prod (_,t,c) -> f (g n) (f n acc t) c | Lambda (_,t,c) -> f (g n) (f n acc t) c | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c @@ -429,7 +431,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with let iter_constr_with_full_binders g f l c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () - | Cast (c,t) -> f l c; f l t + | Cast (c,_, t) -> f l c; f l t | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c @@ -695,7 +697,7 @@ let hdchar env c = | Prod (_,_,c) -> hdrec (k+1) c | Lambda (_,_,c) -> hdrec (k+1) c | LetIn (_,_,_,c) -> hdrec (k+1) c - | Cast (c,_) -> hdrec k c + | Cast (c,_,_) -> hdrec k c | App (f,l) -> hdrec k f | Const kn -> let c = lowercase_first_char (id_of_label (con_label kn)) in @@ -786,6 +788,7 @@ let ids_of_rel_context sign = Sign.fold_rel_context (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign ~init:[] + let ids_of_named_context sign = Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] @@ -793,6 +796,7 @@ let ids_of_context env = (ids_of_rel_context (rel_context env)) @ (ids_of_named_context (named_context env)) + let names_of_rel_context env = List.map (fun (na,_,_) -> na) (rel_context env) @@ -824,7 +828,7 @@ let is_global id = false let is_section_variable id = - try let _ = Sign.lookup_named id (Global.named_context()) in true + try let _ = Global.lookup_named id in true with Not_found -> false let next_global_ident_from allow_secvar id avoid = @@ -934,7 +938,7 @@ let eta_eq_constr = (* iterator on rel context *) let process_rel_context f env = - let sign = named_context env in + let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in Sign.fold_rel_context f rels ~init:env0 @@ -1006,6 +1010,6 @@ let rec rename_bound_var env l c = | Prod (Anonymous,c1,c2) -> let env' = push_rel (Anonymous,None,c1) env in mkProd (Anonymous, c1, rename_bound_var env' l c2) - | Cast (c,t) -> mkCast (rename_bound_var env l c, t) + | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t) | x -> c diff --git a/pretyping/typing.ml b/pretyping/typing.ml index dd2d781d5..38febedaa 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -112,16 +112,16 @@ let rec execute env evd cstr = let j1 = execute env evd c1 in let j2 = execute env evd c2 in let j2 = type_judgment env j2 in - let _ = judge_of_cast env j1 j2 in + let _ = judge_of_cast env j1 DEFAULTcast j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in let j3 = execute env1 evd c3 in judge_of_letin env name j1 j2 j3 - | Cast (c,t) -> + | Cast (c,k,t) -> let cj = execute env evd c in let tj = execute env evd t in let tj = type_judgment env tj in - let j, _ = judge_of_cast env cj tj in + let j, _ = judge_of_cast env cj k tj in j and execute_recdef env evd (names,lar,vdef) = diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index e653345da..6a0ea6096 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -42,7 +42,7 @@ let clenv_cast_meta clenv = let rec crec u = match kind_of_term u with | App _ | Case _ -> crec_hd u - | Cast (c,_) when isMeta c -> u + | Cast (c,_,_) when isMeta c -> u | _ -> map_constr crec u and crec_hd u = @@ -51,7 +51,7 @@ let clenv_cast_meta clenv = (try let b = Typing.meta_type clenv.env mv in if occur_meta b then u - else mkCast (mkMeta mv, b) + else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index 0c9fe0119..26848802e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -69,77 +69,45 @@ let with_check = Options.with_option check (* Implementation of the structural rules (moving and deleting hypotheses around) *) -let check_clear_forward cleared_ids used_ids whatfor = - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^" is used in "^whatfor)) - used_ids - (* The Clear tactic: it scans the context for hypotheses to be removed (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) let clear_hyps ids gl = let env = Global.env() in - let (nhyps,rmv) = - Sign.fold_named_context - (fun (id,c,ty as d) (hyps,rmv) -> - if List.mem id ids then - (hyps,id::rmv) - else begin - check_clear_forward rmv (global_vars_set_of_decl env d) - ("hypothesis "^string_of_id id); - (add_named_decl d hyps, rmv) - end) - gl.evar_hyps - ~init:(empty_named_context,[]) in + let (nhyps,cleared_ids) = + let fcheck cleared_ids (id,_,_ as d) = + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^ + " is used in hypothesis "^string_of_id id)) + (global_vars_set_of_decl env d) in + clear_hyps ids fcheck gl.evar_hyps in let ncl = gl.evar_concl in - check_clear_forward rmv (global_vars_set env ncl) "conclusion"; + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^" is used in conclusion")) + (global_vars_set env ncl); mk_goal nhyps ncl (* The ClearBody tactic *) (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) tail)] *) + returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = - let found = ref false in - let sign' = - fold_named_context_both_sides - (fun head (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f head d tail - end else - add_named_decl d head) - sign ~init:empty_named_context - in - if (not !check) || !found then sign' else error "No such assumption" - -(* Same but with whole environment *) -let apply_to_hyp2 env id f = - let found = ref false in - let env' = - fold_named_context_both_sides - (fun env (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f env d tail - end else - push_named d env) - (named_context env) ~init:(reset_context env) - in - if (not !check) || !found then env' else error "No such assumption" + try apply_to_hyp sign id f + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let apply_to_hyp_and_dependent_on sign id f g = - let found = ref false in - let sign = - Sign.fold_named_context - (fun (idc,_,_ as d) oldest -> - if idc = id then (found := true; add_named_decl (f d) oldest) - else if !found then add_named_decl (g d) oldest - else add_named_decl d oldest) - sign ~init:empty_named_context - in - if (not !check) || !found then sign else error "No such assumption" + try apply_to_hyp_and_dependent_on sign id f g + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -154,26 +122,24 @@ let recheck_typability (what,id) env sigma t = ("The correctness of "^s^" relies on the body of "^(string_of_id id)) let remove_hyp_body env sigma id = - apply_to_hyp2 env id - (fun env (_,c,t) tail -> - match c with - | None -> error ((string_of_id id)^" is not a local definition") - | Some c -> - let env' = push_named (id,None,t) env in - if !check then - ignore - (Sign.fold_named_context - (fun (id',c,t as d) env'' -> - (match c with - | None -> - recheck_typability (Some id',id) env'' sigma t - | Some b -> - let b' = mkCast (b,t) in - recheck_typability (Some id',id) env'' sigma b'); - push_named d env'') - (List.rev tail) ~init:env'); - env') - + let sign = + apply_to_hyp_and_dependent_on (named_context_val env) id + (fun (_,c,t) _ -> + match c with + | None -> error ((string_of_id id)^" is not a local definition") + | Some c ->(id,None,t)) + (fun (id',c,t as d) sign -> + (if !check then + begin + let env = reset_with_named_context sign env in + match c with + | None -> recheck_typability (Some id',id) env sigma t + | Some b -> + let b' = mkCast (b,DEFAULTcast, t) in + recheck_typability (Some id',id) env sigma b' + end;d)) + in + reset_with_named_context sign env (* Auxiliary functions for primitive MOVE tactic * @@ -223,9 +189,16 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = moverec first' middle' right in if toleft then - List.rev_append (moverec [] [declfrom] left) right + let right = + List.fold_right push_named_context_val right empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right (moverec [] [declfrom] left) else - List.rev_append left (moverec [] [declfrom] right) + let right = + List.fold_right push_named_context_val + (moverec [] [declfrom] right) empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right left let check_backward_dependencies sign d = if not (Idset.for_all @@ -247,8 +220,8 @@ let check_forward_dependencies id tail = let rename_hyp id1 id2 sign = apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) -> (id2,b,t)) - (map_named_declaration (replace_vars [id1,mkVar id2])) + (fun (_,b,t) _ -> (id2,b,t)) + (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) let replace_hyp sign id d = apply_to_hyp sign id @@ -256,13 +229,17 @@ let replace_hyp sign id d = if !check then (check_backward_dependencies sign d; check_forward_dependencies id tail); - add_named_decl d sign) + d) +(* why we dont check that id does not appear in tail ??? *) let insert_after_hyp sign id d = - apply_to_hyp sign id - (fun sign d' _ -> - if !check then check_backward_dependencies sign d; - add_named_decl d (add_named_decl d' sign)) + try + insert_after_hyp sign id d + (fun sign -> + if !check then check_backward_dependencies sign d) + with Hyp_not_found -> + if !check then error "No such assumption" + else sign (************************************************************************) (************************************************************************) @@ -274,7 +251,7 @@ variables only in Application and Case *) let collect_meta_variables c = let rec collrec acc c = match kind_of_term c with | Meta mv -> mv::acc - | Cast(c,_) -> collrec acc c + | Cast(c,_,_) -> collrec acc c | (App _| Case _) -> fold_constr collrec acc c | _ -> acc in @@ -303,7 +280,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = raise (RefinerError (OccurMetaGoal conclty)); (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty - | Cast (t,ty) -> + | Cast (t,_, ty) -> check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; mk_refgoals sigma goal goalacc ty t @@ -338,11 +315,11 @@ and mk_hdgoals sigma goal goalacc trm = let env = evar_env goal in let hyps = goal.evar_hyps in match kind_of_term trm with - | Cast (c,ty) when isMeta c -> + | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; (mk_goal hyps (nf_betaiota ty))::goalacc,ty - | Cast (t,ty) -> + | Cast (t,_, ty) -> check_typability env sigma ty; mk_refgoals sigma goal goalacc ty t @@ -393,13 +370,13 @@ let error_use_instantiate () = let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id - (fun sign (_,c,ct) _ -> + (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if !check && not (is_conv env sigma bt ct) then error ("Incorrect change of the type of "^(string_of_id id)); if !check && not (option_compare (is_conv env sigma) b c) then error ("Incorrect change of the body of "^(string_of_id id)); - add_named_decl d sign) + d) (************************************************************************) @@ -413,18 +390,18 @@ let prim_refiner r sigma goal = match r with (* Logical rules *) | Intro id -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); - let sg = mk_goal (add_named_decl (id,None,c1) sign) + let sg = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in [sg] | LetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let sg = - mk_goal (add_named_decl (id,Some c1,t1) sign) + mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in [sg] | _ -> @@ -446,11 +423,11 @@ let prim_refiner r sigma goal = raise (RefinerError IntroNeedsProduct)) | Cut (b,id,t) -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; if occur_meta t then error_use_instantiate(); let sg1 = mk_goal sign (nf_betaiota t) in - let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in + let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in if b then [sg1;sg2] else [sg2;sg1] | FixRule (f,n,rest) -> @@ -474,9 +451,9 @@ let prim_refiner r sigma goal = if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); - if !check && mem_named_context f sign then + if !check && mem_named_context f (named_context_of_val sign) then error "name already used in the environment"; - mk_sign (add_named_decl (f,None,ar) sign) oth + mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all in @@ -499,11 +476,11 @@ let prim_refiner r sigma goal = let rec mk_sign sign = function | (f,ar)::oth -> (try - (let _ = Sign.lookup_named f sign in + (let _ = lookup_named_val f sign in error "name already used in the environment") with | Not_found -> - mk_sign (add_named_decl (f,None,ar) sign) oth) + 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 @@ -516,7 +493,7 @@ let prim_refiner r sigma goal = sgl (* Conversion rules *) - | Convert_concl cl' -> + | Convert_concl (cl',_) -> check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in @@ -537,18 +514,20 @@ let prim_refiner r sigma goal = if !check then recheck_typability (None,id) env' sigma cl; env' in - let sign' = named_context (List.fold_left clear_aux env ids) in + let sign' = named_context_val (List.fold_left clear_aux env ids) in let sg = mk_goal sign' cl in [sg] | Move (withdep, hfrom, hto) -> - let (left,right,declfrom,toleft) = split_sign hfrom hto sign in + let (left,right,declfrom,toleft) = + split_sign hfrom hto (named_context_of_val sign) in let hyps' = move_after withdep toleft (left,declfrom,right) hto in [mk_goal hyps' cl] | Rename (id1,id2) -> - if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then + if !check & id1 <> id2 && + List.mem id2 (ids_of_named_context (named_context_of_val sign)) then error ((string_of_id id2)^" is already used"); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in @@ -622,9 +601,9 @@ let prim_extractor subfun vl pft = plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) - | Some (Prim (Convert_concl _),[pf]) -> - subfun vl pf - + | Some (Prim (Convert_concl (t,k)),[pf]) -> + if k = DEFAULTcast then subfun vl pf + else mkCast (subfun vl pf,k,cl) | Some (Prim (Convert_hyp _),[pf]) -> subfun vl pf diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index eca13c56c..8871e7e00 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -76,7 +76,7 @@ val get_undo : unit -> int option declare the built constructions as a coercion or a setoid morphism) *) val start_proof : - identifier -> goal_kind -> named_context -> constr + identifier -> goal_kind -> named_context_val -> constr -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 73a6bd9a8..1b691e258 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -21,7 +21,7 @@ open Proof_type (* This module declares readable constraints, and a few utilities on constraints and proof trees *) -val mk_goal : named_context -> constr -> goal +val mk_goal : named_context_val -> constr -> goal val rule_of_proof : proof_tree -> rule val ref_of_proof : proof_tree -> (rule * proof_tree list) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index c20b01636..db3c0e7e2 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -32,7 +32,7 @@ type prim_rule = | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr - | Convert_concl of types + | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index cecda38c5..e22273058 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -32,7 +32,7 @@ type prim_rule = | FixRule of identifier * int * (identifier * int * constr) list | Cofix of identifier * (identifier * constr) list | Refine of constr - | Convert_concl of types + | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of identifier list | ThinBody of identifier list diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 8e02a7b27..2fed1cd2c 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -20,6 +20,13 @@ open Tacred open Closure open RedFlags + +(* call by value normalisation function using the virtual machine *) +let cbv_vm env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Vconv.cbv_vm env c ctyp + + let set_opaque_const sp = Conv_oracle.set_opaque_const sp; Csymtable.set_opaque_const sp @@ -45,10 +52,6 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -(* call by value reduction functions using virtual machine *) -let cbv_vm env _ c = - let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in - Vconv.cbv_vm env c ctyp (* Generic reduction: reduction functions used in reduction tactics *) @@ -91,16 +94,19 @@ let declare_red_expr s f = red_expr_tab := Stringmap.add s f !red_expr_tab let reduction_of_red_expr = function - | Red internal -> if internal then try_red_product else red_product - | Hnf -> hnf_constr - | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf - | Simpl None -> nf - | Cbv f -> cbv_norm_flags (make_flag f) - | Lazy f -> clos_norm_flags (make_flag f) - | Unfold ubinds -> unfoldn ubinds - | Fold cl -> fold_commands cl - | Pattern lp -> pattern_occs lp + | Red internal -> + if internal then (try_red_product,DEFAULTcast) + else (red_product,DEFAULTcast) + | Hnf -> (hnf_constr,DEFAULTcast) + | Simpl (Some (_,c as lp)) -> + (contextually (is_reference c) lp nf,DEFAULTcast) + | Simpl None -> (nf,DEFAULTcast) + | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) + | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) + | Unfold ubinds -> (unfoldn ubinds,DEFAULTcast) + | Fold cl -> (fold_commands cl,DEFAULTcast) + | Pattern lp -> (pattern_occs lp,DEFAULTcast) | ExtraRedExpr s -> - (try Stringmap.find s !red_expr_tab + (try (Stringmap.find s !red_expr_tab,DEFAULTcast) with Not_found -> error("unknown user-defined reduction \""^s^"\"")) - | CbvVm -> cbv_vm + | CbvVm -> (cbv_vm ,VMcast) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 7146f7f5e..1c9393d7f 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -14,12 +14,11 @@ open Closure open Rawterm open Reductionops -(* Call by value strategy (uses virtual machine) *) -val cbv_vm : reduction_function type red_expr = (constr, evaluable_global_reference) red_expr_gen -val reduction_of_red_expr : red_expr -> reduction_function +val reduction_of_red_expr : red_expr -> reduction_function * cast_kind +(* [true] if we should use the vm to verify the reduction *) val declare_red_expr : string -> reduction_function -> unit @@ -29,3 +28,8 @@ val set_transparent_const : constant -> unit val set_opaque_var : identifier -> unit val set_transparent_var : identifier -> unit + + + +(* call by value normalisation function using the virtual machine *) +val cbv_vm : reduction_function diff --git a/proofs/refiner.ml b/proofs/refiner.ml index fecddbefb..fa29f5b4d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -41,7 +41,7 @@ let and_status = List.fold_left (+) 0 (* Getting env *) let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps -let pf_hyps gls = (sig_it gls).evar_hyps +let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps (* Normalizing evars in a goal. Called by tactic Local_constraints (i.e. when the sigma of the proof tree changes). Detect if the @@ -51,11 +51,7 @@ let norm_goal sigma gl = let ncl = red_fun gl.evar_concl in let ngl = { evar_concl = ncl; - evar_hyps = - Sign.fold_named_context - (fun (d,b,ty) sign -> - add_named_decl (d, option_app red_fun b, red_fun ty) sign) - gl.evar_hyps ~init:empty_named_context; + evar_hyps = map_named_val red_fun gl.evar_hyps; evar_body = gl.evar_body} in if ngl = gl then None else Some ngl @@ -288,11 +284,11 @@ let extract_open_proof sigma pf = (fun id -> try let n = list_index id vl in (n,id) with Not_found -> failwith "caught") - (ids_of_named_context goal.evar_hyps) in + (ids_of_named_context (named_context_of_val goal.evar_hyps)) in let sorted_rels = Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in let sorted_env = - List.map (fun (n,id) -> (n,Sign.lookup_named id goal.evar_hyps)) + List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps)) sorted_rels in let abs_concl = List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c) @@ -776,7 +772,8 @@ let extract_pftreestate pts = else str "Attempt to save a proof with existential variables still non-instantiated"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in - strong whd_betaiotaevar env pts.tpfsigma pfterm + strong whd_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm + (* strong whd_betaiotaevar env pts.tpfsigma pfterm *) (*** local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm ***) @@ -900,7 +897,7 @@ let tclINFO (tac : tactic) gls = let (sgl,v) as res = tac gls in begin try let pf = v (List.map leaf (sig_it sgl)) in - let sign = (sig_it gls).evar_hyps in + let sign = named_context_of_val (sig_it gls).evar_hyps in msgnl (hov 0 (str" == " ++ !pp_info (project gls) sign pf)) with e when catchable_exception e -> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 816fdf932..7ac7b185b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -92,7 +92,7 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string let pf_reduction_of_red_expr gls re c = - reduction_of_red_expr re (pf_env gls) (project gls) c + (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply @@ -115,7 +115,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) -let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, c2))) +let pf_check_type gls c1 c2 = + ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) (************************************) (* Tactics handling a list of goals *) @@ -190,8 +191,8 @@ let internal_cut_rev_no_check id t gl = let refine_no_check c gl = refiner (Prim (Refine c)) gl -let convert_concl_no_check c gl = - refiner (Prim (Convert_concl c)) gl +let convert_concl_no_check c sty gl = + refiner (Prim (Convert_concl (c,sty))) gl let convert_hyp_no_check d gl = refiner (Prim (Convert_hyp d)) gl @@ -218,8 +219,10 @@ let mutual_cofix f others gl = let rename_bound_var_goal gls = let { evar_hyps = sign; evar_concl = cl } = sig_it gls in - let ids = ids_of_named_context sign in - convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls + let ids = ids_of_named_context (named_context_of_val sign) in + convert_concl_no_check + (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls + (* Versions with consistency checks *) @@ -229,7 +232,7 @@ let intro_replacing id = with_check (intro_replacing_no_check id) let internal_cut d t = with_check (internal_cut_no_check d t) let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t) let refine c = with_check (refine_no_check c) -let convert_concl d = with_check (convert_concl_no_check d) +let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin l = with_check (thin_no_check l) let thin_body c = with_check (thin_body_no_check c) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 66cb97fac..817f934db 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -127,7 +127,7 @@ val intro_replacing_no_check : identifier -> tactic val internal_cut_no_check : identifier -> types -> tactic val internal_cut_rev_no_check : identifier -> types -> tactic val refine_no_check : constr -> tactic -val convert_concl_no_check : types -> tactic +val convert_concl_no_check : types -> cast_kind -> tactic val convert_hyp_no_check : named_declaration -> tactic val thin_no_check : identifier list -> tactic val thin_body_no_check : identifier list -> tactic @@ -145,10 +145,7 @@ val intro_replacing : identifier -> tactic val internal_cut : identifier -> types -> tactic val internal_cut_rev : identifier -> types -> tactic val refine : constr -> tactic -val convert_concl : constr -> tactic -val convert_hyp : named_declaration -> tactic -val thin : identifier list -> tactic -val convert_concl : types -> tactic +val convert_concl : types -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val thin_body : identifier list -> tactic diff --git a/tactics/auto.ml b/tactics/auto.ml index dd07c2b90..e6d1194a5 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -189,7 +189,7 @@ let make_exact_entry name (c,cty) = { hname=name; pri=0; pat=None; code=Give_exact c }) let dummy_goal = - {it={evar_hyps=empty_named_context;evar_concl=mkProp;evar_body=Evar_empty}; + {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty}; sigma=Evd.empty} let make_apply_entry env sigma (eapply,verbose) name (c,cty) = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index b79e6c608..6cf0cc981 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -89,7 +89,7 @@ let autorewrite_in id tac_main lbas gl = let to_be_cleared = ref false in fun dir cstr gl -> let last_hyp_id = - match gl.Evd.it.Evd.evar_hyps with + match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis : " ^ (string_of_id !id)) @@ -98,7 +98,7 @@ let autorewrite_in id tac_main lbas gl = let gls = (fst gl').Evd.it in match gls with g::_ -> - (match g.Evd.evar_hyps with + (match Environ.named_context_of_val g.Evd.evar_hyps with (lastid,_,_)::_ -> if last_hyp_id <> lastid then begin diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 52f5f011a..e3cb25632 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -85,7 +85,8 @@ let e_constructor_tac boundopt i lbind gl = end; let cons = mkConstruct (ith_constructor_of_inductive mind i) in let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in - (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl + (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast +; intros; apply_tac]) gl let e_one_constructor i = e_constructor_tac None i diff --git a/tactics/equality.ml b/tactics/equality.ml index 57d9ab58a..23e4d311c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -690,7 +690,7 @@ let try_delta_expand env sigma t = match kind_of_term c with | Construct _ -> whdt | App (f,_) -> hd_rec f - | Cast (c,_) -> hd_rec c + | Cast (c,_,_) -> hd_rec c | _ -> t in hd_rec whdt @@ -1036,7 +1036,7 @@ let unfold_body x gl = let rfun _ _ c = replace_term xvar xval c in tclTHENLIST [tclMAP (fun h -> reduct_in_hyp rfun h) hl; - reduct_in_concl rfun] gl + reduct_in_concl (rfun,DEFAULTcast)] gl @@ -1088,8 +1088,9 @@ let subst_one x gl = let introtac = function (id,None,_) -> intro_using id | (id,Some hval,htyp) -> - forward true (Name id) (mkCast(replace_term varx rhs hval, - replace_term varx rhs htyp)) in + forward true (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast, + replace_term varx rhs htyp)) + in let need_rewrite = dephyps <> [] || depconcl in tclTHENLIST ((if need_rewrite then diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index a0be2149a..d1a2b40b1 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -34,7 +34,7 @@ let instantiate n rawc ido gl = match ido with ConclLocation () -> evar_list sigma gl.it.evar_concl | HypLocation (id,hloc) -> - let decl = lookup_named id gl.it.evar_hyps in + let decl = Environ.lookup_named_val id gl.it.evar_hyps in match hloc with InHyp -> (match decl with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 60d05ec70..481b78683 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -216,7 +216,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature"); *) - let invSign = named_context invEnv in + let invSign = named_context_val invEnv in let pfs = mk_pftreestate (mk_goal invSign invGoal) in let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in diff --git a/tactics/refine.ml b/tactics/refine.ml index 493232d3c..a6b904c05 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -97,9 +97,9 @@ let replace_by_meta env = function (* quand on introduit une mv on calcule son type *) let ty = match kind_of_term c with | Lambda (Name id,c1,c2) when isCast c2 -> - mkNamedProd id c1 (snd (destCast c2)) + let _,_,t = destCast c2 in mkNamedProd id c1 t | Lambda (Anonymous,c1,c2) when isCast c2 -> - mkArrow c1 (snd (destCast c2)) + let _,_,t = destCast c2 in mkArrow c1 t | _ -> (* (App _ | Case _) -> *) Retyping.get_type_of_with_meta env Evd.empty mm c (* @@ -108,7 +108,7 @@ let replace_by_meta env = function | _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" *) in - mkCast (m,ty),[n,ty],[Some th] + mkCast (m,DEFAULTcast, ty),[n,ty],[Some th] exception NoMeta @@ -138,9 +138,10 @@ let rec compute_metamap env c = match kind_of_term c with | Meta n -> TH (c,[],[None]) - | Cast (m,ty) when isMeta m -> + | Cast (m,_, ty) when isMeta m -> TH (c,[destMeta m,ty],[None]) + (* abstraction => il faut décomposer si le terme dessous n'est pas pur * attention : dans ce cas il faut remplacer (Rel 1) par (Var x) * où x est une variable FRAICHE *) @@ -216,7 +217,7 @@ let rec compute_metamap env c = match kind_of_term c with end (* Cast. Est-ce bien exact ? *) - | Cast (c,t) -> compute_metamap env c + | Cast (c,_,t) -> compute_metamap env c (*let TH (c',mm,sgp) = compute_metamap sign c in TH (mkCast (c',t),mm,sgp) *) @@ -258,7 +259,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | Meta _ , _ -> tclIDTAC gl - | Cast (c,_), _ when isMeta c -> + | Cast (c,_,_), _ when isMeta c -> tclIDTAC gl (* terme pur => refine *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 5cd163364..316f3c276 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1464,7 +1464,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = | (he::tl) as a-> let typnf = Reduction.whd_betadeltaiota env typ in match kind_of_term typnf with - Cast (typ,_) -> + Cast (typ,_,_) -> find_non_dependent_function env c c_args_rev typ f_args_rev a_rev a | Prod (name,s,t) -> @@ -1676,7 +1676,7 @@ let syntactic_but_representation_of_marked_but hole_relation hole_direction = else let c_is_proper = let typ = mkApp (rel_out, [| c ; c |]) in - mkCast (Evarutil.mk_new_meta (),typ) + mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ) in mkApp ((Lazy.force coq_ProperElementToKeep), [| hole_relation ; hole_direction; precise_out ; @@ -1759,7 +1759,8 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in let th' = mkApp (proj, [|impl2; impl1; th|]) in Tactics.refine - (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in + (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) + gl in let if_output_relation_is_if gl = let th = apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp @@ -1767,15 +1768,15 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = in let new_but = Termops.replace_term c1 c2 but in Tactics.refine - (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl - in - if output_relation = (Lazy.force coq_iff_relation) then + (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) + gl in + if output_relation = (Lazy.force coq_iff_relation) then if_output_relation_is_iff gl - else + else if_output_relation_is_if gl with - Optimize -> - !general_rewrite (input_direction = Left2Right) (snd hyp) gl + Optimize -> + !general_rewrite (input_direction = Left2Right) (snd hyp) gl let analyse_hypothesis gl c = let ctype = pf_type_of gl c in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5948da2b8..177c3ffd8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1191,7 +1191,9 @@ open Evd let solvable_by_tactic env evi (ev,args) src = match (!implicit_tactic, src) with | Some tac, (ImplicitArg _ | QuestionMark) - when evi.evar_hyps = Environ.named_context env -> + when + Environ.named_context_of_val evi.evar_hyps = + Environ.named_context env -> let id = id_of_string "H" in start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ()); begin @@ -1510,7 +1512,7 @@ and interp_letin ist gl = function with Not_found -> try let t = tactic_of_value v in - let ndc = Environ.named_context env in + let ndc = Environ.named_context_val env in start_proof id IsLocal ndc typ (fun _ _ -> ()); by t; let (_,({const_entry_body = pft},_,_)) = cook_proof () in @@ -1520,7 +1522,7 @@ and interp_letin ist gl = function delete_proof (dummy_loc,id); errorlabstrm "Tacinterp.interp_letin" (str "Term or fully applied tactic expected in Let") - in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl) + in (id,VConstr (mkCast (csr,DEFAULTcast, typ)))::(interp_letin ist gl tl) (* Interprets the Match Context expressions *) and interp_match_context ist g lz lr lmr = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5079a1010..d1a7507c7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -50,7 +50,7 @@ let rec nb_prod x = match kind_of_term c with Prod(_,_,t) -> count (n+1) t | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_) -> count n c + | Cast(c,_,_) -> count n c | _ -> n in count 0 x @@ -144,8 +144,8 @@ type tactic_reduction = env -> evar_map -> constr -> constr reduction function either to the conclusion or to a certain hypothesis *) -let reduct_in_concl redfun gl = - convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl +let reduct_in_concl (redfun,sty) gl = + convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl let reduct_in_hyp redfun (id,_,(where,where')) gl = let (_,c, ty) = pf_get_hyp gl id in @@ -165,7 +165,7 @@ let reduct_in_hyp redfun (id,_,(where,where')) gl = convert_hyp_no_check (id,Some b',ty') gl let reduct_option redfun = function - | Some id -> reduct_in_hyp redfun id + | Some id -> reduct_in_hyp (fst redfun) id | None -> reduct_in_concl redfun (* The following tactic determines whether the reduction @@ -188,7 +188,8 @@ let change_on_subterm cv_pb t = function | Some occl -> contextually false occl (change_and_check Reduction.CONV t) let change_in_concl occl t = - reduct_in_concl (change_on_subterm Reduction.CUMUL t occl) + reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast) + let change_in_hyp occl t = reduct_in_hyp (change_on_subterm Reduction.CONV t occl) @@ -205,22 +206,23 @@ let change occl c cls = onClauses (change_option occl c) cls (* Pour usage interne (le niveau User est pris en compte par reduce) *) -let red_in_concl = reduct_in_concl red_product +let red_in_concl = reduct_in_concl (red_product,DEFAULTcast) let red_in_hyp = reduct_in_hyp red_product -let red_option = reduct_option red_product -let hnf_in_concl = reduct_in_concl hnf_constr +let red_option = reduct_option (red_product,DEFAULTcast) +let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast) let hnf_in_hyp = reduct_in_hyp hnf_constr -let hnf_option = reduct_option hnf_constr -let simpl_in_concl = reduct_in_concl nf +let hnf_option = reduct_option (hnf_constr,DEFAULTcast) +let simpl_in_concl = reduct_in_concl (nf,DEFAULTcast) let simpl_in_hyp = reduct_in_hyp nf -let simpl_option = reduct_option nf -let normalise_in_concl = reduct_in_concl compute +let simpl_option = reduct_option (nf,DEFAULTcast) +let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast) let normalise_in_hyp = reduct_in_hyp compute -let normalise_option = reduct_option compute -let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname) -let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) -let unfold_option loccname = reduct_option (unfoldn loccname) -let pattern_option l = reduct_option (pattern_occs l) +let normalise_option = reduct_option (compute,DEFAULTcast) +let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast) +let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast) +let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) +let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast) +let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) @@ -346,7 +348,9 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = let rec aux ccl = match pf_lookup_hypothesis_as_renamed env ccl h with | None when red -> - aux (Redexpr.reduction_of_red_expr (Red true) env (project gl) ccl) + aux + ((fst (Redexpr.reduction_of_red_expr (Red true))) + env (project gl) ccl) | x -> x in try aux (pf_concl gl) @@ -433,7 +437,7 @@ let rec intros_rmove = function * of the type of a term. *) let apply_type hdcty argl gl = - refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl + refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl let apply_term hdc argl gl = refine (applist (hdc,argl)) gl @@ -443,7 +447,7 @@ let bring_hyps hyps = else (fun gl -> let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in - let f = mkCast (Evarutil.mk_new_meta(),newcl) in + let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in refine_no_check (mkApp (f, instance_from_named_context hyps)) gl) (* Resolution with missing arguments *) @@ -749,7 +753,7 @@ let letin_tac with_eq name c occs gl = let t = refresh_universes (pf_type_of gl c) in let newcl = mkNamedLetIn id c t ccl in tclTHENLIST - [ convert_concl_no_check newcl; + [ convert_concl_no_check newcl DEFAULTcast; intro_gen (IntroMustBe id) lastlhyp true; if with_eq then tclIDTAC else thin_body [id]; tclMAP convert_hyp_no_check depdecls ] gl @@ -882,7 +886,8 @@ let constructor_tac boundopt i lbind gl = end; let cons = mkConstruct (ith_constructor_of_inductive mind i) in let apply_tac = apply_with_bindings (cons,lbind) in - (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl + (tclTHENLIST + [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl let one_constructor i = constructor_tac None i @@ -1391,7 +1396,8 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl = let c = mkVar varname in let indclause = make_clenv_binding gl (c,typ) NoBindings in let elimclause = - make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in + make_clenv_binding gl + (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in elimination_clause_scheme true elimclause indclause gl let make_up_names7 n ind (old_style,cname) = @@ -1900,9 +1906,9 @@ let abstract_subproof name tac gls = (fun (id,_,_ as d) (s1,s2) -> if mem_named_context id current_sign & interpretable_as_section_decl (Sign.lookup_named id current_sign) d - then (s1,add_named_decl d s2) + then (s1,push_named_context_val d s2) else (add_named_decl d s1,s2)) - global_sign (empty_named_context,empty_named_context) in + global_sign (empty_named_context,empty_named_context_val) in let na = next_global_ident_away false name (pf_ids_of_hyps gls) in let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in if occur_existential concl then diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b03a79dd..f3da4a8c9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -46,7 +46,7 @@ exception Bound val introduction : identifier -> tactic val refine : constr -> tactic -val convert_concl : constr -> tactic +val convert_concl : constr -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val mutual_fix : @@ -110,8 +110,8 @@ val exact_proof : Topconstr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic -val reduct_option : tactic_reduction -> simple_clause -> tactic -val reduct_in_concl : tactic_reduction -> tactic +val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic +val reduct_in_concl : tactic_reduction * cast_kind -> tactic val change_in_concl : constr occurrences option -> constr -> tactic val change_in_hyp : constr occurrences option -> constr -> hyp_location -> tactic @@ -124,9 +124,10 @@ val hnf_option : simple_clause -> tactic val simpl_in_concl : tactic val simpl_in_hyp : hyp_location -> tactic val simpl_option : simple_clause -> tactic -val normalise_in_concl: tactic +val normalise_in_concl : tactic val normalise_in_hyp : hyp_location -> tactic val normalise_option : simple_clause -> tactic +val normalise_vm_in_concl : tactic val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic val unfold_in_hyp : (int list * evaluable_global_reference) list -> hyp_location -> tactic @@ -250,3 +251,4 @@ val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic + diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 3ee0ee430..1c95f7fdc 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -28,7 +28,7 @@ type 'a t = (global_reference,constr_pattern,'a) Dn.t let decomp = let rec decrec acc c = match kind_of_term c with | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Cast (c1,_) -> decrec acc c1 + | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in decrec [] diff --git a/toplevel/class.ml b/toplevel/class.ml index eb767694b..8512e00c5 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -178,7 +178,7 @@ let get_target t ind = let prods_of t = let rec aux acc d = match kind_of_term d with | Prod (_,c1,c2) -> aux (c1::acc) c2 - | Cast (c,_) -> aux acc c + | Cast (c,_,_) -> aux acc c | _ -> (d,acc) in aux [] t @@ -244,7 +244,7 @@ let build_id_coercion idf_opt source = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - { const_entry_body = mkCast (val_f, typ_f); + { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()} in diff --git a/toplevel/command.ml b/toplevel/command.ml index 0a97baf8b..0c916f703 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -75,7 +75,7 @@ let rec destSubCast c = match kind_of_term c with let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u) | LetIn (x,b,t,c) -> let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u) - | Cast (b,u) -> (b,u) + | Cast (b,_, u) -> (b,u) | _ -> assert false let rec adjust_conclusion a cs = function @@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = | Some comtyp -> (* We use a cast to avoid troubles with evars in comtyp *) (* that can only be resolved knowing com *) - let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in + let b = abstract_rawconstr (mkCastC (com,DEFAULTcast,comtyp)) bl in let (body,typ) = destSubCast (interp_constr sigma env b) in { const_entry_body = body; const_entry_type = Some typ; @@ -124,7 +124,7 @@ let red_constant_entry bl ce = function | Some red -> let body = ce.const_entry_body in { ce with const_entry_body = - under_binders (Global.env()) (reduction_of_red_expr red) + under_binders (Global.env()) (fst (reduction_of_red_expr red)) (length_of_raw_binders bl) body } diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7633e168f..97ba5c81c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -144,9 +144,9 @@ let re_exec is_ide = (*s options for the virtual machine *) -let boxed_val = ref true -let boxed_def = ref true -let use_vm = ref true +let boxed_val = ref false +let boxed_def = ref false +let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); @@ -173,7 +173,7 @@ let parse_args is_ide = | [] -> () | "-impredicative-set" :: rem -> - set_engagement Environ.ImpredicativeSet; parse rem + set_engagement Declarations.ImpredicativeSet; parse rem | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () @@ -239,13 +239,7 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem - | "-unboxed-values" :: rem -> - boxed_val := false; parse rem - | "-boxed-definitions" :: rem -> - boxed_def := true; parse rem - | "-no-vm" :: rem -> use_vm := false; parse rem - | "-draw-vm-instr" :: rem -> Vm.set_drawinstr (); - Options.set_print_bytecodes true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Options.print_emacs := true; parse rem | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0 diff --git a/toplevel/record.ml b/toplevel/record.ml index 6b412ea68..88bd4650c 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -37,7 +37,7 @@ let interp_decl sigma env = function | Vernacexpr.DefExpr((_,id),c,t) -> let c = match t with | None -> c - | Some t -> mkCastC (c,t) + | Some t -> mkCastC (c,DEFAULTcast,t) in let j = judgment_of_rawconstr Evd.empty env c in (id,Some j.uj_val, j.uj_type) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 124ad03c6..a93e6fd5e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -764,14 +764,6 @@ let _ = let _ = declare_bool_option - { optsync = false; - optname = "print the bytecode of global definitions"; - optkey = (SecondaryTable ("Print","Bytecode")); - optread = Options.print_bytecodes; - optwrite = (fun b -> Options.set_print_bytecodes b) } - -let _ = - declare_bool_option { optsync = true; optname = "use of virtual machine inside the kernel"; optkey = (SecondaryTable ("Virtual","Machine")); @@ -780,7 +772,7 @@ let _ = let _ = declare_bool_option - { optsync = false; + { optsync = true; optname = "use of boxed definitions"; optkey = (SecondaryTable ("Boxed","Definitions")); optread = Options.boxed_definitions; @@ -888,7 +880,7 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (out_some !pcoq).print_check j else msg (print_judgment env j) | Some r -> - let redfun = reduction_of_red_expr (interp_redexp env evmap r) in + let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in if !pcoq <> None then (out_some !pcoq).print_eval (redfun env evmap) env rc j else msg (print_eval redfun env j) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 292eb0c3f..91a4f3cb7 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -135,7 +135,7 @@ let rec uri_of_constr c = | RLetIn (_,na,b,c) -> url_string "let "; url_of_name na; url_string "\\def "; uri_of_constr b; url_string " in "; uri_of_constr c - | RCast (_,c,t) -> + | RCast (_,c,_,t) -> uri_of_constr c; url_string ":"; uri_of_constr t | RRec _ | RIf _ | RLetTuple _ | ROrderedCase _ | RCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint" diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 6bae2537e..5f3cda588 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -214,7 +214,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c,t) -> c, t + | CCast(_,c,_,t) -> c, t | _ -> c, CHole dummy_loc in hov 1 (surround (pr_lname na ++ pr_opt_type pr_c topt ++ @@ -595,7 +595,7 @@ let rec pr sep inherited a = | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom - | CCast (_,a,b) -> + | CCast (_,a,_,b) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), lcast | CNotation (_,"( _ )",[t]) -> @@ -634,7 +634,7 @@ let rec prod_constr_expr c = function let rec strip_context n iscast t = if n = 0 then - [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t + [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t else match t with | CLambdaN (loc,(nal,t)::bll,c) -> let n' = List.length nal in @@ -657,7 +657,7 @@ let rec strip_context n iscast t = | CArrow (loc,t,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawAssum ([loc,Anonymous],t) :: bl', c - | CCast (_,c,_) -> strip_context n false c + | CCast (_,c,_,_) -> strip_context n false c | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index a8d0b1390..1e4b26103 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -609,7 +609,7 @@ let rec pr_vernac = function (bl2,body,mt()) | Some ty -> let bl2,body,ty' = extract_def_binders c ty in - (bl2,CCast (dummy_loc,body,ty'), + (bl2,CCast (dummy_loc,body,Term.DEFAULTcast,ty'), spc() ++ str":" ++ pr_sep_com spc (pr_type_env_n (Global.env()) (bl@bl2)) ty') in @@ -791,7 +791,8 @@ let rec pr_vernac = function spc() ++ str "{struct " ++ pr_name name ++ str"}" else mt() in let bl,ppc = - pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in + pr_lconstr_env_n rec_sign true bl + (CCast(dummy_loc,def,Term.DEFAULTcast,type_)) in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_type c) type_ ++ str" :=" ++ brk(1,1) ++ ppc ++ |