diff options
42 files changed, 662 insertions, 537 deletions
@@ -54,12 +54,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \ kernel/declarations.cmi kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.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/retroknowledge.cmi kernel/names.cmi \ @@ -89,9 +89,6 @@ 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/environ.cmi kernel/entries.cmi \ @@ -122,6 +119,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/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \ interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \ @@ -142,7 +142,7 @@ parsing/ppdecl_proof.cmi: lib/pp.cmi kernel/environ.cmi proofs/decl_expr.cmi parsing/pptactic.cmi: interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi pretyping/pretyping.cmi \ interp/ppextend.cmi lib/pp.cmi library/libnames.cmi interp/genarg.cmi \ - kernel/environ.cmi + pretyping/evd.cmi kernel/environ.cmi parsing/ppvernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi pretyping/rawterm.cmi parsing/pptactic.cmi \ interp/ppextend.cmi parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi \ @@ -278,7 +278,7 @@ tactics/autorewrite.cmi: kernel/term.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/names.cmi tactics/btermdn.cmi: kernel/term.cmi pretyping/pattern.cmi tactics/contradiction.cmi: kernel/term.cmi pretyping/rawterm.cmi \ - proofs/proof_type.cmi kernel/names.cmi + proofs/proof_type.cmi kernel/names.cmi interp/genarg.cmi tactics/decl_interp.cmi: tactics/tacinterp.cmi kernel/mod_subst.cmi \ pretyping/evd.cmi kernel/environ.cmi proofs/decl_mode.cmi \ proofs/decl_expr.cmi @@ -304,13 +304,12 @@ tactics/extraargs.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacexpr.cmo tactics/setoid_replace.cmi \ kernel/retroknowledge.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ parsing/pcoq.cmi kernel/names.cmi -tactics/extratactics.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ - proofs/tacexpr.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ - kernel/names.cmi interp/genarg.cmi +tactics/extratactics.cmi: pretyping/rawterm.cmi proofs/proof_type.cmi \ + pretyping/evd.cmi tactics/hiddentac.cmi: kernel/term.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo proofs/redexpr.cmi \ pretyping/rawterm.cmi proofs/proof_type.cmi kernel/names.cmi \ - interp/genarg.cmi + interp/genarg.cmi pretyping/evd.cmi tactics/hipattern.cmi: lib/util.cmi kernel/term.cmi proofs/tacmach.cmi \ kernel/sign.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ pretyping/pattern.cmi kernel/names.cmi pretyping/evd.cmi \ @@ -371,12 +370,12 @@ 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 \ lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ pretyping/reductionops.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 contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \ @@ -386,9 +385,9 @@ contrib/cc/ccproof.cmi: kernel/term.cmi kernel/names.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 \ @@ -456,10 +455,10 @@ contrib/funind/functional_principles_types.cmi: kernel/term.cmi \ contrib/funind/indfun_common.cmi: kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi library/libnames.cmi \ kernel/entries.cmi library/decl_kinds.cmo -contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \ - pretyping/rawterm.cmi kernel/names.cmi contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \ kernel/names.cmi library/libnames.cmi +contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \ + pretyping/rawterm.cmi kernel/names.cmi contrib/funind/tacinvutils.cmi: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi tactics/refine.cmi \ @@ -496,7 +495,6 @@ contrib/rtauto/refl_tauto.cmi: kernel/term.cmi proofs/tacmach.cmi \ contrib/subtac/context.cmi: kernel/term.cmi kernel/names.cmi contrib/subtac/eterm.cmi: lib/util.cmi kernel/term.cmi proofs/tacmach.cmi \ kernel/names.cmi pretyping/evd.cmi -contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi contrib/subtac/subtac_cases.cmi: lib/util.cmi kernel/term.cmi \ pretyping/rawterm.cmi kernel/names.cmi pretyping/inductiveops.cmi \ pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ @@ -509,6 +507,7 @@ contrib/subtac/subtac_command.cmi: toplevel/vernacexpr.cmo \ contrib/subtac/subtac_errors.cmi: lib/util.cmi lib/pp.cmi contrib/subtac/subtac_interp_fixpoint.cmi: lib/util.cmi interp/topconstr.cmi \ lib/pp.cmi kernel/names.cmi library/libnames.cmi +contrib/subtac/subtac.cmi: toplevel/vernacexpr.cmo lib/util.cmi contrib/subtac/subtac_obligations.cmi: lib/util.cmi interp/topconstr.cmi \ kernel/term.cmi proofs/tacexpr.cmo proofs/proof_type.cmi kernel/names.cmi contrib/subtac/subtac_pretyping.cmi: interp/topconstr.cmi kernel/term.cmi \ @@ -568,6 +567,16 @@ 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 lib/pp.cmi proofs/pfedit.cmi \ + ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \ + proofs/decl_mode.cmi config/coq_config.cmi 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 lib/pp.cmx proofs/pfedit.cmx \ + ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \ + proofs/decl_mode.cmx config/coq_config.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 lib/system.cmi \ @@ -592,16 +601,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ config/coq_config.cmx toplevel/cerrors.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 lib/pp.cmi proofs/pfedit.cmi \ - ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \ - proofs/decl_mode.cmi config/coq_config.cmi 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 lib/pp.cmx proofs/pfedit.cmx \ - ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \ - proofs/decl_mode.cmx config/coq_config.cmx ide/coq_commands.cmx \ - ide/coq.cmx ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/find_phrase.cmo: ide/preferences.cmi ide/ideutils.cmi ide/find_phrase.cmx: ide/preferences.cmx ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -790,6 +789,14 @@ 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/closure.cmx \ kernel/inductive.cmi +kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ + kernel/retroknowledge.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 \ + kernel/retroknowledge.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 \ @@ -804,14 +811,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \ kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \ kernel/cemitcodes.cmx kernel/mod_typing.cmi -kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ - kernel/retroknowledge.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 \ - kernel/retroknowledge.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/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \ kernel/names.cmi kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \ @@ -916,10 +915,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 @@ -928,24 +927,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/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/decl_kinds.cmo: lib/util.cmi -library/decl_kinds.cmx: lib/util.cmx 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 \ @@ -978,6 +967,8 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ library/global.cmx kernel/environ.cmx kernel/entries.cmx \ kernel/declarations.cmx library/declaremods.cmi +library/decl_kinds.cmo: lib/util.cmi +library/decl_kinds.cmx: lib/util.cmx library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \ library/summary.cmi kernel/reduction.cmi library/nametab.cmi \ kernel/names.cmi library/libobject.cmi library/libnames.cmi \ @@ -1060,6 +1051,14 @@ 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/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 @@ -1099,11 +1098,11 @@ parsing/g_decl_mode.cmx: interp/topconstr.cmx kernel/term.cmx \ parsing/pcoq.cmx kernel/names.cmx library/libnames.cmx interp/genarg.cmx \ proofs/decl_expr.cmi parsing/g_intsyntax.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \ - interp/notation.cmi kernel/names.cmi library/libnames.cmi lib/bigint.cmi \ - parsing/g_intsyntax.cmi + interp/notation.cmi kernel/names.cmi library/libnames.cmi \ + pretyping/evd.cmi lib/bigint.cmi parsing/g_intsyntax.cmi parsing/g_intsyntax.cmx: lib/util.cmx pretyping/rawterm.cmx lib/pp.cmx \ - interp/notation.cmx kernel/names.cmx library/libnames.cmx lib/bigint.cmx \ - parsing/g_intsyntax.cmi + interp/notation.cmx kernel/names.cmx library/libnames.cmx \ + pretyping/evd.cmx lib/bigint.cmx parsing/g_intsyntax.cmi parsing/g_ltac.cmo: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi lib/pp.cmi parsing/pcoq.cmi \ kernel/names.cmi @@ -1226,32 +1225,34 @@ parsing/pptactic.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \ parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi pretyping/pattern.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi library/global.cmi interp/genarg.cmi \ - parsing/egrammar.cmi lib/dyn.cmi kernel/closure.cmi parsing/pptactic.cmi + pretyping/evd.cmi parsing/egrammar.cmi lib/dyn.cmi kernel/closure.cmi \ + parsing/pptactic.cmi parsing/pptactic.cmx: lib/util.cmx interp/topconstr.cmx pretyping/termops.cmx \ kernel/term.cmx proofs/tactic_debug.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx parsing/printer.cmx interp/ppextend.cmx \ parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx pretyping/pattern.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx library/global.cmx interp/genarg.cmx \ - parsing/egrammar.cmx lib/dyn.cmx kernel/closure.cmx parsing/pptactic.cmi + pretyping/evd.cmx parsing/egrammar.cmx lib/dyn.cmx kernel/closure.cmx \ + parsing/pptactic.cmi parsing/ppvernac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi parsing/pptactic.cmi interp/ppextend.cmi \ parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ interp/modintern.cmi library/libnames.cmi library/lib.cmi \ - library/impargs.cmi library/goptions.cmi library/global.cmi \ - interp/genarg.cmi parsing/extend.cmi parsing/egrammar.cmi \ - library/declaremods.cmi library/decl_kinds.cmo parsing/ppvernac.cmi + library/goptions.cmi library/global.cmi interp/genarg.cmi \ + parsing/extend.cmi parsing/egrammar.cmi library/declaremods.cmi \ + library/decl_kinds.cmo parsing/ppvernac.cmi parsing/ppvernac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx parsing/pptactic.cmx interp/ppextend.cmx \ parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ interp/modintern.cmx library/libnames.cmx library/lib.cmx \ - library/impargs.cmx library/goptions.cmx library/global.cmx \ - interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \ - library/declaremods.cmx library/decl_kinds.cmx parsing/ppvernac.cmi + library/goptions.cmx library/global.cmx interp/genarg.cmx \ + parsing/extend.cmx parsing/egrammar.cmx library/declaremods.cmx \ + library/decl_kinds.cmx parsing/ppvernac.cmi parsing/prettyp.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi interp/syntax_def.cmi kernel/sign.cmi \ kernel/safe_typing.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ @@ -1740,13 +1741,13 @@ proofs/refiner.cmx: lib/util.cmx kernel/type_errors.cmx pretyping/termops.cmx \ pretyping/reductionops.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ lib/pp.cmx proofs/logic.cmx library/global.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx kernel/environ.cmx proofs/refiner.cmi -proofs/tacexpr.cmo: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ - pretyping/rawterm.cmi pretyping/pattern.cmi library/nametab.cmi \ - kernel/names.cmi library/libnames.cmi interp/genarg.cmi lib/dyn.cmi \ +proofs/tacexpr.cmo: lib/util.cmi interp/topconstr.cmi pretyping/rawterm.cmi \ + pretyping/pattern.cmi library/nametab.cmi kernel/names.cmi \ + library/libnames.cmi interp/genarg.cmi pretyping/evd.cmi lib/dyn.cmi \ library/decl_kinds.cmo -proofs/tacexpr.cmx: lib/util.cmx interp/topconstr.cmx kernel/term.cmx \ - pretyping/rawterm.cmx pretyping/pattern.cmx library/nametab.cmx \ - kernel/names.cmx library/libnames.cmx interp/genarg.cmx lib/dyn.cmx \ +proofs/tacexpr.cmx: lib/util.cmx interp/topconstr.cmx pretyping/rawterm.cmx \ + pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ + library/libnames.cmx interp/genarg.cmx pretyping/evd.cmx lib/dyn.cmx \ library/decl_kinds.cmx proofs/tacmach.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ kernel/term.cmi pretyping/tacred.cmi proofs/tacexpr.cmo kernel/sign.cmi \ @@ -1902,36 +1903,36 @@ tactics/eauto.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/refiner.cmi kernel/reduction.cmi pretyping/rawterm.cmi \ proofs/proof_type.cmi proofs/proof_trees.cmi parsing/pptactic.cmi \ lib/pp.cmi parsing/pcoq.cmi pretyping/pattern.cmi kernel/names.cmi \ - library/nameops.cmi proofs/logic.cmi parsing/lexer.cmi library/global.cmi \ - interp/genarg.cmi lib/explore.cmi proofs/evar_refiner.cmi \ - parsing/egrammar.cmi kernel/declarations.cmi proofs/clenvtac.cmi \ - pretyping/clenv.cmi toplevel/cerrors.cmi tactics/auto.cmi \ - tactics/eauto.cmi + library/nameops.cmi proofs/logic.cmi parsing/lexer.cmi \ + tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ + lib/explore.cmi proofs/evar_refiner.cmi parsing/egrammar.cmi \ + kernel/declarations.cmi proofs/clenvtac.cmi pretyping/clenv.cmi \ + toplevel/cerrors.cmi tactics/auto.cmi tactics/eauto.cmi tactics/eauto.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx kernel/reduction.cmx pretyping/rawterm.cmx \ proofs/proof_type.cmx proofs/proof_trees.cmx parsing/pptactic.cmx \ lib/pp.cmx parsing/pcoq.cmx pretyping/pattern.cmx kernel/names.cmx \ - library/nameops.cmx proofs/logic.cmx parsing/lexer.cmx library/global.cmx \ - interp/genarg.cmx lib/explore.cmx proofs/evar_refiner.cmx \ - parsing/egrammar.cmx kernel/declarations.cmx proofs/clenvtac.cmx \ - pretyping/clenv.cmx toplevel/cerrors.cmx tactics/auto.cmx \ - tactics/eauto.cmi + library/nameops.cmx proofs/logic.cmx parsing/lexer.cmx \ + tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ + lib/explore.cmx proofs/evar_refiner.cmx parsing/egrammar.cmx \ + kernel/declarations.cmx proofs/clenvtac.cmx pretyping/clenv.cmx \ + toplevel/cerrors.cmx tactics/auto.cmx tactics/eauto.cmi tactics/elim.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ proofs/tacexpr.cmo proofs/refiner.cmi kernel/reduction.cmi \ proofs/proof_type.cmi parsing/printer.cmi lib/pp.cmi kernel/names.cmi \ library/libnames.cmi pretyping/inductiveops.cmi tactics/hipattern.cmi \ - tactics/hiddentac.cmi interp/genarg.cmi kernel/environ.cmi \ - pretyping/clenv.cmi tactics/elim.cmi + tactics/hiddentac.cmi interp/genarg.cmi pretyping/evd.cmi \ + kernel/environ.cmi pretyping/clenv.cmi tactics/elim.cmi tactics/elim.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ proofs/tacexpr.cmx proofs/refiner.cmx kernel/reduction.cmx \ proofs/proof_type.cmx parsing/printer.cmx lib/pp.cmx kernel/names.cmx \ library/libnames.cmx pretyping/inductiveops.cmx tactics/hipattern.cmx \ - tactics/hiddentac.cmx interp/genarg.cmx kernel/environ.cmx \ - pretyping/clenv.cmx tactics/elim.cmi + tactics/hiddentac.cmx interp/genarg.cmx pretyping/evd.cmx \ + kernel/environ.cmx pretyping/clenv.cmx tactics/elim.cmi tactics/eqdecide.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo proofs/refiner.cmi pretyping/rawterm.cmi \ @@ -2027,11 +2028,13 @@ tactics/extratactics.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ tactics/hiddentac.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo proofs/refiner.cmi \ proofs/redexpr.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ - interp/genarg.cmi tactics/evar_tactics.cmi tactics/hiddentac.cmi + interp/genarg.cmi pretyping/evd.cmi tactics/evar_tactics.cmi \ + tactics/hiddentac.cmi tactics/hiddentac.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ proofs/tacmach.cmx proofs/tacexpr.cmx proofs/refiner.cmx \ proofs/redexpr.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ - interp/genarg.cmx tactics/evar_tactics.cmx tactics/hiddentac.cmi + interp/genarg.cmx pretyping/evd.cmx tactics/evar_tactics.cmx \ + tactics/hiddentac.cmi tactics/hipattern.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \ pretyping/rawterm.cmi proofs/proof_trees.cmi lib/pp.cmi \ @@ -2153,16 +2156,16 @@ tactics/tacinterp.cmo: lib/util.cmi pretyping/typing.cmi interp/topconstr.cmi \ pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ pretyping/pretyping.cmi pretyping/pretype_errors.cmi parsing/pptactic.cmi \ lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi pretyping/pattern.cmi \ - lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ - kernel/mod_subst.cmi pretyping/matching.cmi proofs/logic.cmi \ - library/libobject.cmi library/libnames.cmi library/lib.cmi \ - tactics/leminv.cmi tactics/inv.cmi pretyping/inductiveops.cmi \ - tactics/hiddentac.cmi lib/gmap.cmi library/global.cmi interp/genarg.cmi \ - parsing/g_xml.cmo pretyping/evd.cmi tactics/equality.cmi \ - kernel/environ.cmi kernel/entries.cmi tactics/elim.cmi lib/dyn.cmi \ - tactics/dhyp.cmi pretyping/detyping.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/constrintern.cmi kernel/closure.cmi \ - tactics/auto.cmi tactics/tacinterp.cmi + lib/options.cmi interp/notation.cmi library/nametab.cmi kernel/names.cmi \ + library/nameops.cmi kernel/mod_subst.cmi pretyping/matching.cmi \ + proofs/logic.cmi library/libobject.cmi library/libnames.cmi \ + library/lib.cmi tactics/leminv.cmi tactics/inv.cmi \ + pretyping/inductiveops.cmi tactics/hiddentac.cmi lib/gmap.cmi \ + library/global.cmi interp/genarg.cmi parsing/g_xml.cmo pretyping/evd.cmi \ + tactics/equality.cmi kernel/environ.cmi kernel/entries.cmi \ + tactics/elim.cmi lib/dyn.cmi tactics/dhyp.cmi pretyping/detyping.cmi \ + kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \ + kernel/closure.cmi tactics/auto.cmi tactics/tacinterp.cmi tactics/tacinterp.cmx: lib/util.cmx pretyping/typing.cmx interp/topconstr.cmx \ pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ @@ -2172,16 +2175,16 @@ tactics/tacinterp.cmx: lib/util.cmx pretyping/typing.cmx interp/topconstr.cmx \ pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ pretyping/pretyping.cmx pretyping/pretype_errors.cmx parsing/pptactic.cmx \ lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx pretyping/pattern.cmx \ - lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ - kernel/mod_subst.cmx pretyping/matching.cmx proofs/logic.cmx \ - library/libobject.cmx library/libnames.cmx library/lib.cmx \ - tactics/leminv.cmx tactics/inv.cmx pretyping/inductiveops.cmx \ - tactics/hiddentac.cmx lib/gmap.cmx library/global.cmx interp/genarg.cmx \ - parsing/g_xml.cmx pretyping/evd.cmx tactics/equality.cmx \ - kernel/environ.cmx kernel/entries.cmx tactics/elim.cmx lib/dyn.cmx \ - tactics/dhyp.cmx pretyping/detyping.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/constrintern.cmx kernel/closure.cmx \ - tactics/auto.cmx tactics/tacinterp.cmi + lib/options.cmx interp/notation.cmx library/nametab.cmx kernel/names.cmx \ + library/nameops.cmx kernel/mod_subst.cmx pretyping/matching.cmx \ + proofs/logic.cmx library/libobject.cmx library/libnames.cmx \ + library/lib.cmx tactics/leminv.cmx tactics/inv.cmx \ + pretyping/inductiveops.cmx tactics/hiddentac.cmx lib/gmap.cmx \ + library/global.cmx interp/genarg.cmx parsing/g_xml.cmx pretyping/evd.cmx \ + tactics/equality.cmx kernel/environ.cmx kernel/entries.cmx \ + tactics/elim.cmx lib/dyn.cmx tactics/dhyp.cmx pretyping/detyping.cmx \ + kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \ + kernel/closure.cmx tactics/auto.cmx tactics/tacinterp.cmi tactics/tacticals.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi proofs/refiner.cmi \ kernel/reduction.cmi lib/pp.cmi pretyping/pattern.cmi kernel/names.cmi \ @@ -2438,16 +2441,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 lib/system.cmi library/states.cmi \ - parsing/ppvernac.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 interp/constrintern.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \ - parsing/ppvernac.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 interp/constrintern.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 \ @@ -2512,6 +2505,16 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \ lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \ toplevel/vernacinterp.cmi +toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \ + parsing/ppvernac.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 interp/constrintern.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \ + parsing/ppvernac.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 interp/constrintern.cmx toplevel/vernac.cmi toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \ interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \ @@ -2560,6 +2563,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \ tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.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 \ @@ -2574,12 +2583,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 @@ -3054,38 +3057,6 @@ contrib/funind/functional_principles_types.cmx: lib/util.cmx \ kernel/environ.cmx kernel/entries.cmx library/declare.cmx \ kernel/declarations.cmx library/decl_kinds.cmx toplevel/command.cmx \ kernel/closure.cmx contrib/funind/functional_principles_types.cmi -contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ - kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ - kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ - proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ - library/states.cmi kernel/sign.cmi contrib/recdef/recdef.cmo \ - contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \ - parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi \ - interp/notation.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi library/impargs.cmi \ - tactics/hiddentac.cmi library/global.cmi \ - contrib/funind/functional_principles_types.cmi \ - contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \ - tactics/equality.cmi kernel/environ.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ - toplevel/command.cmi toplevel/cerrors.cmi -contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ - kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ - library/states.cmx kernel/sign.cmx contrib/recdef/recdef.cmx \ - contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \ - parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx \ - interp/notation.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \ - contrib/funind/indfun_common.cmx library/impargs.cmx \ - tactics/hiddentac.cmx library/global.cmx \ - contrib/funind/functional_principles_types.cmx \ - contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \ - tactics/equality.cmx kernel/environ.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \ - toplevel/command.cmx toplevel/cerrors.cmx contrib/funind/indfun_common.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi library/summary.cmi proofs/refiner.cmi \ pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ @@ -3134,6 +3105,38 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ contrib/funind/functional_principles_types.cmx pretyping/evd.cmx \ parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \ toplevel/cerrors.cmx +contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ + kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ + proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ + library/states.cmi kernel/sign.cmi contrib/recdef/recdef.cmo \ + contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \ + parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi \ + interp/notation.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \ + contrib/funind/indfun_common.cmi library/impargs.cmi \ + tactics/hiddentac.cmi library/global.cmi \ + contrib/funind/functional_principles_types.cmi \ + contrib/funind/functional_principles_proofs.cmi pretyping/evd.cmi \ + tactics/equality.cmi kernel/environ.cmi kernel/declarations.cmi \ + library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ + toplevel/command.cmi toplevel/cerrors.cmi +contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ + kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ + proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ + library/states.cmx kernel/sign.cmx contrib/recdef/recdef.cmx \ + contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \ + parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx \ + interp/notation.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \ + contrib/funind/indfun_common.cmx library/impargs.cmx \ + tactics/hiddentac.cmx library/global.cmx \ + contrib/funind/functional_principles_types.cmx \ + contrib/funind/functional_principles_proofs.cmx pretyping/evd.cmx \ + tactics/equality.cmx kernel/environ.cmx kernel/declarations.cmx \ + library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \ + toplevel/command.cmx toplevel/cerrors.cmx contrib/funind/invfun.cmo: toplevel/vernacentries.cmi lib/util.cmi \ pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tauto.cmo tactics/tactics.cmi tactics/tacticals.cmi \ @@ -3180,6 +3183,16 @@ contrib/funind/merge.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ pretyping/evd.cmx kernel/environ.cmx pretyping/detyping.cmx \ kernel/declarations.cmx interp/constrintern.cmx interp/constrextern.cmx \ toplevel/command.cmx +contrib/funind/rawtermops.cmo: lib/util.cmi kernel/term.cmi \ + pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi pretyping/inductiveops.cmi \ + contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \ + interp/coqlib.cmi contrib/funind/rawtermops.cmi +contrib/funind/rawtermops.cmx: lib/util.cmx kernel/term.cmx \ + pretyping/rawterm.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx pretyping/inductiveops.cmx \ + contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \ + interp/coqlib.cmx contrib/funind/rawtermops.cmi contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ pretyping/typing.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tacinterp.cmi lib/system.cmi kernel/sign.cmi \ @@ -3204,16 +3217,6 @@ contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ pretyping/detyping.cmx kernel/declarations.cmx interp/coqlib.cmx \ interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ contrib/funind/rawterm_to_relation.cmi -contrib/funind/rawtermops.cmo: lib/util.cmi kernel/term.cmi \ - pretyping/rawterm.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi pretyping/inductiveops.cmi \ - contrib/funind/indfun_common.cmi library/global.cmi pretyping/evd.cmi \ - interp/coqlib.cmi contrib/funind/rawtermops.cmi -contrib/funind/rawtermops.cmx: lib/util.cmx kernel/term.cmx \ - pretyping/rawterm.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx pretyping/inductiveops.cmx \ - contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \ - interp/coqlib.cmx contrib/funind/rawtermops.cmi contrib/funind/tacinvutils.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi pretyping/reductionops.cmi \ parsing/printer.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \ @@ -3236,11 +3239,11 @@ contrib/interface/blast.cmo: toplevel/vernacinterp.cmi \ parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \ parsing/pcoq.cmi contrib/interface/pbp.cmi pretyping/pattern.cmi \ kernel/names.cmi library/nameops.cmi proofs/logic.cmi \ - kernel/inductive.cmi tactics/hipattern.cmi library/global.cmi \ - lib/explore.cmi pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ - tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \ - toplevel/command.cmi pretyping/clenv.cmi tactics/auto.cmi \ - contrib/interface/blast.cmi + kernel/inductive.cmi tactics/hipattern.cmi tactics/hiddentac.cmi \ + library/global.cmi lib/explore.cmi pretyping/evd.cmi tactics/equality.cmi \ + kernel/environ.cmi tactics/eauto.cmi library/declare.cmi \ + kernel/declarations.cmi toplevel/command.cmi pretyping/clenv.cmi \ + tactics/auto.cmi contrib/interface/blast.cmi contrib/interface/blast.cmx: toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \ @@ -3251,11 +3254,11 @@ contrib/interface/blast.cmx: toplevel/vernacinterp.cmx \ parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \ parsing/pcoq.cmx contrib/interface/pbp.cmx pretyping/pattern.cmx \ kernel/names.cmx library/nameops.cmx proofs/logic.cmx \ - kernel/inductive.cmx tactics/hipattern.cmx library/global.cmx \ - lib/explore.cmx pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ - tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ - toplevel/command.cmx pretyping/clenv.cmx tactics/auto.cmx \ - contrib/interface/blast.cmi + kernel/inductive.cmx tactics/hipattern.cmx tactics/hiddentac.cmx \ + library/global.cmx lib/explore.cmx pretyping/evd.cmx tactics/equality.cmx \ + kernel/environ.cmx tactics/eauto.cmx library/declare.cmx \ + kernel/declarations.cmx toplevel/command.cmx pretyping/clenv.cmx \ + tactics/auto.cmx contrib/interface/blast.cmi contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo toplevel/vernacentries.cmi toplevel/vernac.cmi \ @@ -3388,6 +3391,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 \ + 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 \ + contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/typing.cmi kernel/typeops.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \ @@ -3410,14 +3421,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ kernel/declarations.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 \ - 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 \ - contrib/interface/ascent.cmi contrib/interface/translate.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \ kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \ @@ -3525,33 +3528,35 @@ contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \ kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/rawterm.cmi \ - proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \ - parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ - lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi library/lib.cmi tactics/hiddentac.cmi \ - library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ - tactics/equality.cmi kernel/environ.cmi kernel/entries.cmi \ - tactics/elim.cmi parsing/egrammar.cmi tactics/eauto.cmi \ - library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \ - interp/coqlib.cmi interp/constrintern.cmi toplevel/command.cmi \ - kernel/closure.cmi toplevel/cerrors.cmi tactics/auto.cmi + tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \ + pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ + pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ + library/nameops.cmi library/libnames.cmi library/lib.cmi \ + tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ + kernel/entries.cmi tactics/elim.cmi parsing/egrammar.cmi \ + tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \ + library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \ + toplevel/command.cmi kernel/closure.cmi toplevel/cerrors.cmi \ + tactics/auto.cmi contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/rawterm.cmx \ - proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \ - parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ - lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx library/lib.cmx tactics/hiddentac.cmx \ - library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ - tactics/equality.cmx kernel/environ.cmx kernel/entries.cmx \ - tactics/elim.cmx parsing/egrammar.cmx tactics/eauto.cmx \ - library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \ - interp/coqlib.cmx interp/constrintern.cmx toplevel/command.cmx \ - kernel/closure.cmx toplevel/cerrors.cmx tactics/auto.cmx + tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/reductionops.cmx \ + pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ + pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \ + library/nameops.cmx library/libnames.cmx library/lib.cmx \ + tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ + kernel/entries.cmx tactics/elim.cmx parsing/egrammar.cmx \ + tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ + library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \ + toplevel/command.cmx kernel/closure.cmx toplevel/cerrors.cmx \ + tactics/auto.cmx contrib/ring/g_quote.cmo: lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/ring/quote.cmo parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi interp/genarg.cmi parsing/egrammar.cmi \ @@ -3716,38 +3721,6 @@ contrib/subtac/g_subtac.cmx: toplevel/vernacinterp.cmx \ kernel/reduction.cmx lib/pp.cmx parsing/pcoq.cmx lib/options.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx -contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ - kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \ - kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ - contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \ - contrib/subtac/subtac_errors.cmi contrib/subtac/subtac_command.cmi \ - contrib/subtac/subtac_coercion.cmi kernel/sign.cmi \ - pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ - parsing/printer.cmi pretyping/pretype_errors.cmi parsing/ppconstr.cmi \ - lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi lib/options.cmi \ - library/nametab.cmi kernel/names.cmi library/library.cmi \ - library/libnames.cmi library/lib.cmi toplevel/himsg.cmi \ - library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ - pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \ - lib/dyn.cmi pretyping/detyping.cmi library/decl_kinds.cmo \ - interp/coqlib.cmi contrib/subtac/context.cmi toplevel/command.cmi \ - pretyping/classops.cmi toplevel/cerrors.cmi contrib/subtac/subtac.cmi -contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \ - kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ - contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \ - contrib/subtac/subtac_errors.cmx contrib/subtac/subtac_command.cmx \ - contrib/subtac/subtac_coercion.cmx kernel/sign.cmx \ - pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ - parsing/printer.cmx pretyping/pretype_errors.cmx parsing/ppconstr.cmx \ - lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx lib/options.cmx \ - library/nametab.cmx kernel/names.cmx library/library.cmx \ - library/libnames.cmx library/lib.cmx toplevel/himsg.cmx \ - library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ - pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \ - lib/dyn.cmx pretyping/detyping.cmx library/decl_kinds.cmx \ - interp/coqlib.cmx contrib/subtac/context.cmx toplevel/command.cmx \ - pretyping/classops.cmx toplevel/cerrors.cmx contrib/subtac/subtac.cmi contrib/subtac/subtac_cases.cmo: lib/util.cmi kernel/typeops.cmi \ kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \ contrib/subtac/subtac_utils.cmi kernel/sign.cmi pretyping/retyping.cmi \ @@ -3852,6 +3825,38 @@ contrib/subtac/subtac_interp_fixpoint.cmx: lib/util.cmx kernel/typeops.cmx \ contrib/subtac/eterm.cmx kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \ contrib/subtac/context.cmx pretyping/classops.cmx \ contrib/subtac/subtac_interp_fixpoint.cmi +contrib/subtac/subtac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ + kernel/typeops.cmi kernel/type_errors.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ + contrib/subtac/subtac_utils.cmi contrib/subtac/subtac_pretyping.cmi \ + contrib/subtac/subtac_errors.cmi contrib/subtac/subtac_command.cmi \ + contrib/subtac/subtac_coercion.cmi kernel/sign.cmi \ + pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ + parsing/printer.cmi pretyping/pretype_errors.cmi parsing/ppconstr.cmi \ + lib/pp.cmi proofs/pfedit.cmi pretyping/pattern.cmi lib/options.cmi \ + library/nametab.cmi kernel/names.cmi library/library.cmi \ + library/libnames.cmi library/lib.cmi toplevel/himsg.cmi \ + library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ + pretyping/evarconv.cmi contrib/subtac/eterm.cmi kernel/environ.cmi \ + lib/dyn.cmi pretyping/detyping.cmi library/decl_kinds.cmo \ + interp/coqlib.cmi contrib/subtac/context.cmi toplevel/command.cmi \ + pretyping/classops.cmi toplevel/cerrors.cmi contrib/subtac/subtac.cmi +contrib/subtac/subtac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ + kernel/typeops.cmx kernel/type_errors.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ + contrib/subtac/subtac_utils.cmx contrib/subtac/subtac_pretyping.cmx \ + contrib/subtac/subtac_errors.cmx contrib/subtac/subtac_command.cmx \ + contrib/subtac/subtac_coercion.cmx kernel/sign.cmx \ + pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ + parsing/printer.cmx pretyping/pretype_errors.cmx parsing/ppconstr.cmx \ + lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx lib/options.cmx \ + library/nametab.cmx kernel/names.cmx library/library.cmx \ + library/libnames.cmx library/lib.cmx toplevel/himsg.cmx \ + library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ + pretyping/evarconv.cmx contrib/subtac/eterm.cmx kernel/environ.cmx \ + lib/dyn.cmx pretyping/detyping.cmx library/decl_kinds.cmx \ + interp/coqlib.cmx contrib/subtac/context.cmx toplevel/command.cmx \ + pretyping/classops.cmx toplevel/cerrors.cmx contrib/subtac/subtac.cmi contrib/subtac/subtac_obligations.cmo: lib/util.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ library/summary.cmi contrib/subtac/subtac_utils.cmi proofs/refiner.cmi \ @@ -3872,6 +3877,26 @@ contrib/subtac/subtac_obligations.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/entries.cmx library/declare.cmx library/decl_kinds.cmx \ toplevel/command.cmx tactics/auto.cmx \ contrib/subtac/subtac_obligations.cmi +contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \ + kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \ + contrib/subtac/subtac_cases.cmi kernel/sign.cmi pretyping/retyping.cmi \ + pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ + pretyping/pretyping.cmi pretyping/pretype_errors.cmi lib/pp.cmi \ + pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \ + library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ + pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \ + kernel/environ.cmi lib/dyn.cmi kernel/declarations.cmi \ + pretyping/coercion.cmi pretyping/classops.cmi +contrib/subtac/subtac_pretyping_F.cmx: lib/util.cmx kernel/typeops.cmx \ + kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \ + contrib/subtac/subtac_cases.cmx kernel/sign.cmx pretyping/retyping.cmx \ + pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ + pretyping/pretyping.cmx pretyping/pretype_errors.cmx lib/pp.cmx \ + pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \ + library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ + pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \ + kernel/environ.cmx lib/dyn.cmx kernel/declarations.cmx \ + pretyping/coercion.cmx pretyping/classops.cmx contrib/subtac/subtac_pretyping.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ kernel/typeops.cmi kernel/type_errors.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi contrib/subtac/subtac_utils.cmi \ @@ -3900,26 +3925,6 @@ contrib/subtac/subtac_pretyping.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ kernel/environ.cmx lib/dyn.cmx interp/coqlib.cmx \ contrib/subtac/context.cmx interp/constrintern.cmx toplevel/command.cmx \ pretyping/classops.cmx contrib/subtac/subtac_pretyping.cmi -contrib/subtac/subtac_pretyping_F.cmo: lib/util.cmi kernel/typeops.cmi \ - kernel/type_errors.cmi pretyping/termops.cmi kernel/term.cmi \ - contrib/subtac/subtac_cases.cmi kernel/sign.cmi pretyping/retyping.cmi \ - pretyping/reductionops.cmi pretyping/recordops.cmi pretyping/rawterm.cmi \ - pretyping/pretyping.cmi pretyping/pretype_errors.cmi lib/pp.cmi \ - pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \ - library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ - pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \ - kernel/environ.cmi lib/dyn.cmi kernel/declarations.cmi \ - pretyping/coercion.cmi pretyping/classops.cmi -contrib/subtac/subtac_pretyping_F.cmx: lib/util.cmx kernel/typeops.cmx \ - kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \ - contrib/subtac/subtac_cases.cmx kernel/sign.cmx pretyping/retyping.cmx \ - pretyping/reductionops.cmx pretyping/recordops.cmx pretyping/rawterm.cmx \ - pretyping/pretyping.cmx pretyping/pretype_errors.cmx lib/pp.cmx \ - pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \ - library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ - pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \ - kernel/environ.cmx lib/dyn.cmx kernel/declarations.cmx \ - pretyping/coercion.cmx pretyping/classops.cmx contrib/subtac/subtac_utils.cmo: lib/util.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacexpr.cmo kernel/reduction.cmi \ @@ -3940,18 +3945,12 @@ contrib/subtac/subtac_utils.cmx: lib/util.cmx interp/topconstr.cmx \ pretyping/evarutil.cmx kernel/entries.cmx library/decl_kinds.cmx \ interp/coqlib.cmx interp/constrextern.cmx toplevel/command.cmx \ contrib/subtac/subtac_utils.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 kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \ @@ -3970,6 +3969,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 \ @@ -4010,8 +4015,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/typeops.cmi kernel/term.cmi \ proofs/tacmach.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \ @@ -4042,12 +4045,10 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \ parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/config_file.cmo: ide/utils/config_file.cmi ide/utils/config_file.cmx: ide/utils/config_file.cmi -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_html_config.cmo: ide/utils/configwin_types.cmo \ ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \ ide/utils/config_file.cmi @@ -4058,6 +4059,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/okey.cmi ide/utils/configwin_types.cmo \ ide/utils/configwin_messages.cmo ide/utils/config_file.cmi ide/utils/configwin_ihm.cmx: ide/utils/okey.cmx ide/utils/configwin_types.cmx \ ide/utils/configwin_messages.cmx ide/utils/config_file.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/configwin_keys.cmo \ ide/utils/config_file.cmi ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \ diff --git a/.depend.camlp4 b/.depend.camlp4 index 482cc8786..cd9399563 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -10,7 +10,7 @@ contrib/romega/g_romega.ml: parsing/grammar.cma contrib/ring/g_quote.ml: parsing/grammar.cma contrib/ring/g_ring.ml: parsing/grammar.cma contrib/dp/g_dp.ml: parsing/grammar.cma -contrib/setoid_ring/newring.ml: +contrib/setoid_ring/newring.ml: parsing/grammar.cma contrib/field/field.ml: parsing/grammar.cma contrib/fourier/g_fourier.ml: parsing/grammar.cma contrib/extraction/g_extraction.ml: parsing/grammar.cma diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 8eeb8b642..fac39df93 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -182,11 +182,11 @@ let right_instance_tac inst continue seq= [introf; (fun gls-> split (Rawterm.ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + [inj_open (mkVar (Tacmach.pf_nth_hyp_id gls 1))]) gls); tclSOLVE [wrap 0 true continue (deepen seq)]]; tclTRY assumption] | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclTHEN (split (Rawterm.ImplicitBindings [inj_open t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> tclFAIL 0 (Pp.str "not implemented ... yet") diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index ae3da9523..169542e3c 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -29,20 +29,37 @@ let pr_bindings prc prlc = function Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Rawterm.NoBindings -> mt () - let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) +(* Duplication of printing functions because "'a with_bindings" is + (internally) not uniform in 'a: indeed constr_with_bindings at the + "typed" level has type "open_constr with_bindings" instead of + "constr with_bindings"; hence, its printer cannot be polymorphic in + (prc,prlc)... *) + +let pr_with_bindings_typed prc prlc (c,bl) = + prc c ++ + hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + +let pr_fun_ind_using_typed prc prlc _ opt_c = + match opt_c with + | None -> mt () + | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings_opt - PRINTED BY pr_fun_ind_using + PRINTED BY pr_fun_ind_using_typed + RAW_TYPED AS constr_with_bindings_opt + RAW_PRINTED BY pr_fun_ind_using + GLOB_TYPED AS constr_with_bindings_opt + GLOB_PRINTED BY pr_fun_ind_using | [ "using" constr_with_bindings(c) ] -> [ Some c ] | [ ] -> [ None ] END diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 9ec02d4c4..fbf72805b 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -23,13 +23,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + Util.prlist_with_sep spc (fun (_,c) -> prc c) l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -425,7 +425,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -435,7 +435,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Nameops.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 48c9b9eb4..ab4da05e3 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -166,7 +166,7 @@ let rule_to_ntactic r = let rt = (match r with Nested(Tactic (t,_),_) -> t - | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h) + | Prim (Refine h) -> TacAtom (dummy_loc,TacExact (Tactics.inj_open h)) | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in if rule_is_complex r then (match rt with @@ -1184,8 +1184,8 @@ let rec natural_ntree ig ntree = | TacIntroMove _ -> natural_intros ig lh g gs ltree | TacFix (_,n) -> natural_fix ig lh g gs n ltree | TacSplit (_,NoBindings) -> natural_split ig lh g gs ge [] ltree - | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge l ltree - | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree + | TacSplit(_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree + | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree | (* "Simpl" *)TacReduce (r,cl) -> @@ -1202,17 +1202,17 @@ let rec natural_ntree ig ntree = | TacExtend (_,"InductionIntro",[a]) -> let id=(out_gen wit_ident a) in natural_induction ig lh g gs ge id ltree true - | TacApply (false,(c,_)) -> natural_apply ig lh g gs c ltree - | TacExact c -> natural_exact ig lh g gs c ltree - | TacCut c -> natural_cut ig lh g gs c ltree + | TacApply (false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree + | TacExact c -> natural_exact ig lh g gs (snd c) ltree + | TacCut c -> natural_cut ig lh g gs (snd c) ltree | TacExtend (_,"CutIntro",[a]) -> let _c = out_gen wit_constr a in natural_cutintro ig lh g gs a ltree - | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false + | TacCase (c,_) -> natural_case ig lh g gs ge (snd c) ltree false | TacExtend (_,"CaseIntro",[a]) -> let c = out_gen wit_constr a in natural_case ig lh g gs ge c ltree true - | TacElim ((c,_),_) -> natural_elim ig lh g gs ge c ltree false + | TacElim ((c,_),_) -> natural_elim ig lh g gs ge (snd c) ltree false | TacExtend (_,"ElimIntro",[a]) -> let c = out_gen wit_constr a in natural_elim ig lh g gs ge c ltree true diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 294943f7d..5fd763c36 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -410,7 +410,7 @@ i*) | Negl -> dyn_negl s1 | Allr -> dyn_allr (JT.dest_var t2) | Alll -> dyn_alll s1 s2 (constr_of_jterm t2) - | Exr -> dyn_exr (constr_of_jterm t2) + | Exr -> dyn_exr (Tactics.inj_open (constr_of_jterm t2)) | Exl -> dyn_exl s1 s2 (JT.dest_var t2) | Ax -> T.assumption (*i TCL.tclIDTAC i*) | Truer -> dyn_truer diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 951378d4b..497fcdb6c 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -1221,7 +1221,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac eq1) reflexivity ] + tclTHEN (exists_tac (inj_open eq1)) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 7a2133a02..49791c367 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -416,8 +416,8 @@ let base_leaf_terminate (func:global_reference) eqs expr = [k';h] -> k',h | _ -> assert false in - tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr])); - observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O])); + tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [inj_open expr])); + observe_tac "second split" (split (ImplicitBindings [inj_open (delayed_force coq_O)])); observe_tac "intro k" (h_intro k'); observe_tac "case on k" (tclTHENS @@ -459,7 +459,7 @@ let rec compute_le_proofs = function in apply_with_bindings (le_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id,a]) + ExplicitBindings[dummy_loc,NamedHyp m_id,inj_open a]) g ) [compute_le_proofs tl; @@ -477,7 +477,7 @@ let make_lt_proof pmax le_proof = in apply_with_bindings (le_lt_trans, - ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g) + ExplicitBindings[dummy_loc,NamedHyp m_id, inj_open pmax]) g) [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];; @@ -496,8 +496,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs = tclTHENS (general_rewrite_bindings false (mkVar eq, - ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k; - dummy_loc, NamedHyp def_id, mkVar def]) false) + ExplicitBindings[dummy_loc, NamedHyp k_id, inj_open (mkVar k); + dummy_loc, NamedHyp def_id, inj_open (mkVar def)]) false) [list_cond_rewrite k def pmax eqs le_proofs; observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g ) @@ -515,7 +515,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs let ids = h'::ids in let def = next_global_ident_away true def_id ids in tclTHENLIST - [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max])); + [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [inj_open s_max])); observe_tac "introduce_all_equalities_final intro k" (h_intro k); tclTHENS (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k))) @@ -575,8 +575,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn (match args with [] -> tclTHENLIST - [observe_tac "split" (split(ImplicitBindings - [context_fn (List.map mkVar (List.rev values))])); + [observe_tac "split" (split(ImplicitBindings + [inj_open (context_fn (List.map mkVar (List.rev values)))])); observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])] | arg::args -> @@ -1194,9 +1194,9 @@ let rec introduce_all_values_eq cont_tac functional termine general_rewrite_bindings false (mkVar heq1, ExplicitBindings[dummy_loc,NamedHyp k_id, - f_S(f_S(mkVar pmax)); + inj_open (f_S(f_S(mkVar pmax))); dummy_loc,NamedHyp def_id, - f]) false gls ) + inj_open f]) false gls ) [tclTHENLIST [simpl_iter(); unfold_constr (reference_of_constr functional); @@ -1247,8 +1247,8 @@ let rec introduce_all_values_eq cont_tac functional termine (mkVar heq, ExplicitBindings [dummy_loc, NamedHyp k_id, - f_S(mkVar pmax'); - dummy_loc, NamedHyp def_id, f]) false)) + inj_open (f_S(mkVar pmax')); + dummy_loc, NamedHyp def_id, inj_open f]) false)) g ) [tclIDTAC; diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index fb58a14eb..5a32d2e42 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -231,7 +231,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n]); + (Rawterm.ImplicitBindings [inj_open (mkVar n)]); cont]); ]))) in diff --git a/interp/genarg.ml b/interp/genarg.ml index 2e057e438..d98788eed 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -16,6 +16,7 @@ open Nametab open Rawterm open Topconstr open Term +open Evd type argument_type = (* Basic types *) @@ -47,6 +48,10 @@ type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = AN of 'a | ByNotation of loc * string type rawconstr_and_expr = rawconstr * constr_expr option +type open_constr_expr = unit * constr_expr +type open_rawconstr = unit * rawconstr_and_expr + +type 'a with_ebindings = 'a * open_constr bindings (* Dynamics but tagged by a type expression *) @@ -56,7 +61,7 @@ let dyntab = ref ([] : string list) type rlevel = constr_expr type glevel = rawconstr_and_expr -type tlevel = constr +type tlevel = open_constr type ('a,'b) abstract_argument_type = argument_type @@ -90,10 +95,6 @@ and pr_case_intro_pattern = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" -type open_constr = Evd.evar_map * Term.constr -type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr - let rawwit_bool = BoolArgType let globwit_bool = BoolArgType let wit_bool = BoolArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index db078bfc1..ccaf93d58 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -15,6 +15,7 @@ open Libnames open Rawterm open Topconstr open Term +open Evd type 'a and_short_name = 'a * identifier located option @@ -25,10 +26,11 @@ type 'a or_by_notation = AN of 'a | ByNotation of loc * string (* The [constr_expr] field is [None] in TacDef though *) type rawconstr_and_expr = rawconstr * constr_expr option -type open_constr = Evd.evar_map * Term.constr type open_constr_expr = unit * constr_expr type open_rawconstr = unit * rawconstr_and_expr +type 'a with_ebindings = 'a * open_constr bindings + type intro_pattern_expr = | IntroOrAndPattern of case_intro_pattern_expr | IntroWildcard @@ -106,7 +108,7 @@ ExtraArgType of string '_a '_b type rlevel = constr_expr type glevel = rawconstr_and_expr -type tlevel = constr +type tlevel = open_constr type ('a,'co) abstract_argument_type @@ -176,11 +178,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_bindings,tlevel) abstract_argument_type +val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (constr bindings,tlevel) abstract_argument_type +val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b6c38cf93..d4fa5163e 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -133,6 +133,11 @@ let rec pr_message_token prid = function let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) +let out_bindings = function + | ImplicitBindings l -> ImplicitBindings (List.map snd l) + | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) + | NoBindings -> NoBindings + let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") @@ -244,10 +249,12 @@ let rec pr_generic prc prlc prtac x = pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) (out_gen wit_red_expr x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) - | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) + | ConstrWithBindingsArgType -> + let (c,b) = out_gen wit_constr_with_bindings x in + pr_arg (pr_with_bindings prc prlc) (c,out_bindings b) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) (out_gen wit_bindings x) + pr_arg (pr_bindings_no_with prc prlc) + (out_bindings (out_gen wit_bindings x)) | List0ArgType _ -> hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> @@ -283,7 +290,7 @@ let pr_raw_extend prc prlc prtac = let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen (pr_generic prc prlc prtac) + pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac) (**********************************************************************) (* The tactic printer *) @@ -966,12 +973,12 @@ let strip_prod_binders_rawterm n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n ty = +let strip_prod_binders_constr n (sigma,ty) = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else + if n=0 then (List.rev acc, (sigma,ty)) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],a)::acc) (n-1) b + strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1017,8 +1024,8 @@ and pr_glob_match_rule env t = let typed_printers = (pr_glob_tactic_level, - pr_constr_env, - pr_lconstr_env, + pr_open_constr_env, + pr_open_lconstr_env, pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index cfa035b16..31a626cea 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -17,6 +17,7 @@ open Topconstr open Rawterm open Ppextend open Environ +open Evd val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds @@ -45,7 +46,7 @@ type 'a extra_genarg_printer = val declare_extra_genarg_pprule : ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> - ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit + ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit type grammar_terminals = string option list @@ -73,9 +74,9 @@ val pr_glob_extend: string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> + (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> - string -> closed_generic_argument list -> std_ppcmds + string -> typed_generic_argument list -> std_ppcmds val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds @@ -88,3 +89,7 @@ val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds + +val pr_bindings : + ('constr -> std_ppcmds) -> + ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index df078f302..307e0af23 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -48,10 +48,16 @@ let pr_lconstr_env_at_top env = pr_lconstr_core true env let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env +let pr_open_lconstr_env env (_,c) = pr_lconstr_env env c +let pr_open_constr_env env (_,c) = pr_constr_env env c + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = pr_lconstr_env (Global.env()) t let pr_constr t = pr_constr_env (Global.env()) t +let pr_open_lconstr (_,c) = pr_lconstr c +let pr_open_constr (_,c) = pr_constr c + let pr_type_core at_top env t = pr_constr_expr (extern_type at_top env t) let pr_ltype_core at_top env t = diff --git a/parsing/printer.mli b/parsing/printer.mli index 4e09e0251..1f3f2b0fb 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -35,6 +35,12 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +val pr_open_constr_env : env -> open_constr -> std_ppcmds +val pr_open_constr : open_constr -> std_ppcmds + +val pr_open_lconstr_env : env -> open_constr -> std_ppcmds +val pr_open_lconstr : open_constr -> std_ppcmds + val pr_ltype_env_at_top : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index c629c6c72..929535b76 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -26,11 +26,13 @@ open Pretype_errors open Evarutil open Unification open Mod_subst +open Coercion.Default (* *) let w_coerce env c ctyp target evd = let j = make_judge c ctyp in - let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j (mk_tycon_type target) in + let tycon = mk_tycon_type target in + let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in (evd',j'.uj_val) let pf_env gls = Global.env_of_context gls.it.evar_hyps @@ -42,24 +44,24 @@ let pf_concl gl = gl.it.evar_concl (* Clausal environments *) type clausenv = { - templenv : env; - env : evar_defs; + env : env; + evd : evar_defs; templval : constr freelisted; templtyp : constr freelisted } -let cl_env ce = ce.templenv -let cl_sigma ce = evars_of ce.env +let cl_env ce = ce.env +let cl_sigma ce = evars_of ce.evd let subst_clenv sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; - env = subst_evar_defs_light sub clenv.env; - templenv = clenv.templenv } + evd = subst_evar_defs_light sub clenv.evd; + env = clenv.env } -let clenv_nf_meta clenv c = nf_meta clenv.env c -let clenv_meta_type clenv mv = Typing.meta_type clenv.env mv -let clenv_value clenv = meta_instance clenv.env clenv.templval -let clenv_type clenv = meta_instance clenv.env clenv.templtyp +let clenv_nf_meta clenv c = nf_meta clenv.evd c +let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv +let clenv_value clenv = meta_instance clenv.evd clenv.templval +let clenv_type clenv = meta_instance clenv.evd clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -70,7 +72,7 @@ let clenv_get_type_of ce c = (function | (n,Clval(_,_,typ)) -> (n,typ.rebus) | (n,Cltyp (_,typ)) -> (n,typ.rebus)) - (meta_list ce.env) in + (meta_list ce.evd) in Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c exception NotExtensibleClause @@ -83,13 +85,13 @@ let clenv_push_prod cl = let mv = new_meta () in let dep = dependent (mkRel 1) u in let na' = if dep then na else Anonymous in - let e' = meta_declare mv t ~name:na' cl.env in + let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in { templval = mk_freelisted def; templtyp = mk_freelisted concl; - env = e'; - templenv = cl.templenv } + evd = e'; + env = cl.env } | _ -> raise NotExtensibleClause in clrec typ @@ -146,8 +148,8 @@ let mk_clenv_from_n gls n (c,cty) = let (env,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; - env = env; - templenv = Global.env_of_context gls.it.evar_hyps } + evd = env; + env = Global.env_of_context gls.it.evar_hyps } let mk_clenv_from gls = mk_clenv_from_n gls None @@ -169,15 +171,15 @@ let mentions clenv mv0 = let rec menrec mv1 = mv0 = mv1 || let mlist = - try (fst (meta_fvalue clenv.env mv1)).freemetas + try (fst (meta_fvalue clenv.evd mv1)).freemetas with Anomaly _ | Not_found -> Metaset.empty in meta_exists menrec mlist in menrec -let clenv_defined clenv mv = meta_defined clenv.env mv +let clenv_defined clenv mv = meta_defined clenv.evd mv let error_incompatible_inst clenv mv = - let na = meta_name clenv.env mv in + let na = meta_name clenv.evd mv in match na with Name id -> errorlabstrm "clenv_assign" @@ -192,17 +194,17 @@ let clenv_assign mv rhs clenv = if meta_exists (mentions clenv mv) rhs_fls.freemetas then error "clenv_assign: circularity in unification"; try - if meta_defined clenv.env mv then - if not (eq_constr (fst (meta_fvalue clenv.env mv)).rebus rhs) then + if meta_defined clenv.evd mv then + if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then error_incompatible_inst clenv mv else clenv - else {clenv with env = meta_assign mv (rhs_fls.rebus,ConvUpToEta 0) clenv.env} + else {clenv with evd = meta_assign mv (rhs_fls.rebus,ConvUpToEta 0) clenv.evd} with Not_found -> error "clenv_assign: undefined meta" -let clenv_wtactic f clenv = {clenv with env = f clenv.env } +let clenv_wtactic f clenv = {clenv with evd = f clenv.evd } (* [clenv_dependent hyps_only clenv] @@ -233,7 +235,7 @@ let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas let dependent_metas clenv mvs conclmetas = List.fold_right (fun mv deps -> - Metaset.union deps (clenv_metavars clenv.env mv)) + Metaset.union deps (clenv_metavars clenv.evd mv)) mvs conclmetas let clenv_dependent hyps_only clenv = @@ -250,10 +252,10 @@ let clenv_missing ce = clenv_dependent true ce (******************************************************************) let clenv_unify allow_K cv_pb t1 t2 clenv = - { clenv with env = w_unify allow_K clenv.templenv cv_pb t1 t2 clenv.env } + { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd } -let clenv_unique_resolver allow_K clause gl = - clenv_unify allow_K CUMUL (clenv_type clause) (pf_concl gl) clause +let clenv_unique_resolver allow_K clenv gl = + clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv (* [clenv_pose_dependent_evars clenv] @@ -266,8 +268,8 @@ let clenv_pose_dependent_evars clenv = List.fold_left (fun clenv mv -> let ty = clenv_meta_type clenv mv in - let (evd,evar) = new_evar clenv.env (cl_env clenv) ty in - clenv_assign mv evar {clenv with env=evd}) + let (evd,evar) = new_evar clenv.evd (cl_env clenv) ty in + clenv_assign mv evar {clenv with evd=evd}) clenv dep_mvs @@ -279,8 +281,8 @@ let evar_clenv_unique_resolver clenv gls = let connect_clenv gls clenv = { clenv with - env = evars_reset_evd gls.sigma clenv.env; - templenv = Global.env_of_context gls.it.evar_hyps } + evd = evars_reset_evd gls.sigma clenv.evd; + env = Global.env_of_context gls.it.evar_hyps } (* [clenv_fchain mv clenv clenv'] * @@ -310,8 +312,8 @@ let clenv_fchain mv clenv nextclenv = let clenv' = { templval = clenv.templval; templtyp = clenv.templtyp; - env = meta_merge clenv.env nextclenv.env; - templenv = nextclenv.templenv } in + evd = meta_merge clenv.evd nextclenv.evd; + env = nextclenv.env } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = clenv_unify true CUMUL @@ -327,7 +329,7 @@ let clenv_fchain mv clenv nextclenv = (***************************************************************) (* Bindings *) -type arg_bindings = (int * constr) list +type arg_bindings = (int * open_constr) list (* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, @@ -345,58 +347,58 @@ let meta_of_binder clause loc b t mvs = match b with | NamedHyp s -> if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" + errorlabstrm "" (str "The variable " ++ pr_id s ++ str " occurs more than once in binding"); - meta_with_name clause.env s + meta_with_name clause.evd s | AnonHyp n -> if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" + errorlabstrm "" (str "The position " ++ int n ++ str " occurs more than once in binding"); try List.nth mvs (n-1) with (Failure _|Invalid_argument _) -> - errorlabstrm "clenv_match_args" (str "No such binder") + errorlabstrm "" (str "No such binder") let error_already_defined b = match b with - NamedHyp id -> - errorlabstrm "clenv_match_args" + | NamedHyp id -> + errorlabstrm "" (str "Binder name \"" ++ pr_id id ++ str"\" already defined with incompatible value") | AnonHyp n -> - anomalylabstrm "clenv_match_args" + anomalylabstrm "" (str "Position " ++ int n ++ str" already defined") let clenv_match_args s clause = let mvs = clenv_independent clause in - let rec matchrec clause = function - | [] -> clause - | (loc,b,c)::t -> - let k = meta_of_binder clause loc b t mvs in - if meta_defined clause.env k then - if eq_constr (fst (meta_fvalue clause.env k)).rebus c then - matchrec clause t + let rec matchrec clenv = function + | [] -> clenv + | (loc,b,(sigma,c))::t -> + let k = meta_of_binder clenv loc b t mvs in + if meta_defined clenv.evd k then + if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then + matchrec clenv t else error_already_defined b else - let k_typ = clenv_hnf_constr clause (clenv_meta_type clause k) + let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in (* nf_betaiota was before in type_of - useful to reduce types like (x:A)([x]P u) *) - and c_typ = - clenv_hnf_constr clause - (nf_betaiota (clenv_get_type_of clause c)) in - let cl = + let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in + let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in + let c_typ = clenv_hnf_constr clenv' c_typ in + let clenv'' = (* Try to infer some Meta/Evar from the type of [c] *) - try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause) + try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clenv') with e when precatchable_exception e -> - (* Try to coerce to the type of [k]; cannot merge with the - previous case because Coercion does not handle Meta *) - let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in - try clenv_unify true CONV (mkMeta k) c' clause - with PretypeError (env,CannotUnify (m,n)) -> - Stdpp.raise_with_loc loc - (PretypeError (env,CannotUnifyBindingType (m,n))) - in matchrec cl t + (* Try to coerce to the type of [k]; cannot merge with the + previous case because Coercion does not handle Meta *) + let (evd,c') = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in + try clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd } + with PretypeError (env,CannotUnify (m,n)) -> + Stdpp.raise_with_loc loc + (PretypeError (env,CannotUnifyBindingType (m,n))) + in matchrec clenv'' t in matchrec clause s @@ -408,7 +410,7 @@ let clenv_constrain_with_bindings bl clause = let all_mvs = collect_metas clause.templval.rebus in let rec matchrec clause = function | [] -> clause - | (n,c)::t -> + | (n,(sigma,c))::t -> let k = (try if n > 0 then @@ -421,7 +423,8 @@ let clenv_constrain_with_bindings bl clause = (str"Clause did not have " ++ int n ++ str"-th" ++ str" absolute argument")) in let k_typ = nf_betaiota (clenv_meta_type clause k) in - let c_typ = nf_betaiota (clenv_get_type_of clause c) in + let cl = { clause with evd = evar_merge clause.evd sigma} in + let c_typ = nf_betaiota (clenv_get_type_of cl c) in matchrec (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t in @@ -435,17 +438,16 @@ let clenv_constrain_dep_args hyps_only clause = function let occlist = clenv_dependent hyps_only clause in if List.length occlist = List.length mlist then List.fold_left2 - (fun clenv k c -> + (fun clenv k (sigma,c) -> + let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in + let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in + let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in try - let k_typ = - clenv_hnf_constr clause (clenv_meta_type clause k) in - let c_typ = - clenv_hnf_constr clause (clenv_get_type_of clause c) in (* faire quelque chose avec le sigma retourne ? *) - let (_,c') = w_coerce (cl_env clenv) c c_typ k_typ clenv.env in - clenv_unify true CONV (mkMeta k) c' clenv + let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in + clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd } with _ -> - clenv_unify true CONV (mkMeta k) c clenv) + clenv_unify true CONV (mkMeta k) c clenv') clause occlist mlist else error ("Not the right number of missing arguments (expected " @@ -478,4 +480,4 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - pr_evar_defs clenv.env) + pr_evar_defs clenv.evd) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 944d7d4b3..b9ee5dde4 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -23,17 +23,15 @@ open Rawterm (***************************************************************) (* The Type of Constructions clausale environments. *) -(* [templenv] is the typing context - * [env] is the mapping from metavar and evar numbers to their types +(* [env] is the typing context + * [evd] is the mapping from metavar and evar numbers to their types * and values. * [templval] is the template which we are trying to fill out. * [templtyp] is its type. - * [namenv] is a mapping from metavar numbers to names, for - * use in instantiating metavars by name. *) type clausenv = { - templenv : env; - env : evar_defs; + env : env; + evd : evar_defs; templval : constr freelisted; templtyp : constr freelisted } @@ -89,14 +87,14 @@ val clenv_pose_dependent_evars : clausenv -> clausenv (* bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to start from the rightmost argument of the template. *) -type arg_bindings = (int * constr) list +type arg_bindings = (int * open_constr) list val clenv_independent : clausenv -> metavariable list val clenv_missing : clausenv -> metavariable list (* defines metas corresponding to the name of the bindings *) val clenv_match_args : - constr explicit_bindings -> clausenv -> clausenv + open_constr explicit_bindings -> clausenv -> clausenv val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv (* start with a clenv to refine with a given term with bindings *) @@ -105,10 +103,10 @@ val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv (* the optional int tells how many prods of the lemma have to be used *) (* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int option -> constr * constr -> constr bindings -> + evar_info sigma -> int option -> constr * constr -> open_constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> constr bindings -> clausenv + evar_info sigma -> constr * constr -> open_constr bindings -> clausenv (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where [lmetas] is a list of metas to be applied to a proof of [t] so that diff --git a/pretyping/evd.ml b/pretyping/evd.ml index b9a443317..5d959be8b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -287,6 +287,8 @@ let existential_value (sigma,_) = existential_value sigma let existential_type (sigma,_) = existential_type sigma let existential_opt_value (sigma,_) = existential_opt_value sigma +let merge e e' = fold (fun n v sigma -> add sigma n v) e' e + (*******************************************************************) type open_constr = evar_map * constr @@ -439,6 +441,8 @@ let get_conv_pbs isevars p = {isevars with conv_pbs = pbs1}, pbs +let evar_merge isevars evars = + { isevars with evars = merge isevars.evars evars } (**********************************************************) (* Sort variables *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 8a1f6a53f..f6052b368 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -50,6 +50,8 @@ val mem : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a +val merge : evar_map -> evar_map -> evar_map + val define : evar_map -> evar -> constr -> evar_map val is_evar : evar_map -> evar -> bool @@ -145,6 +147,9 @@ val evar_declare : val evar_define : evar -> constr -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind +(* [evar_merge evd evars] extends the evars of [evd] with [evars] *) +val evar_merge : evar_defs -> evar_map -> evar_defs + (* Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * Environ.env * constr * constr diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b74eac9a5..d991486c4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -367,21 +367,30 @@ let w_merge env with_types mod_delta metas evars evd = in w_merge_rec evd' (metas'@t) evars' else - begin + begin if with_types (* or occur_meta mvty *) then - (let mvty = Typing.meta_type evd mv in - try - let sigma = evars_of evd in - (* why not typing with the metamap ? *) - let nty = Typing.type_of env sigma (nf_meta evd n) in - let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty in - ty_metas := mc @ !ty_metas; - ty_evars := ec @ !ty_evars - with e when precatchable_exception e -> ()); - let evd' = meta_assign mv (n,status) evd in + begin + let mvty = Typing.meta_type evd mv in + try + let sigma = evars_of evd in + (* why not typing with the metamap ? *) + let nty = Typing.type_of env sigma (nf_meta evd n) in + (* unification with arities may induce a too early *) + (* commitment of an evar to an arity of wrong sort *) + if + not (is_arity env sigma mvty) && + not (is_arity env sigma nty) + then + let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty + in + ty_metas := mc @ !ty_metas; + ty_evars := ec @ !ty_evars + with e when precatchable_exception e -> () + end; + let evd' = meta_assign mv (n,status) evd in w_merge_rec evd' t [] - end - + end + and mimick_evar evd mod_delta hdc nargs sp = let ev = Evd.find (evars_of evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in @@ -592,5 +601,5 @@ let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd = error "Cannot solve a second-order unification problem") (* General case: try first order *) - | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd + | _ -> w_typed_unify env cv_pb mod_delta ty1 ty2 evd diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8bba76007..db94fad14 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -49,7 +49,7 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - let b = Typing.meta_type clenv.env mv in + let b = Typing.meta_type clenv.evd mv in if occur_meta b then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) @@ -62,7 +62,7 @@ let clenv_cast_meta clenv = let clenv_refine clenv gls = tclTHEN - (tclEVARS (evars_of clenv.env)) + (tclEVARS (evars_of clenv.evd)) (refine (clenv_cast_meta clenv (clenv_value clenv))) gls diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 20ce39775..dfe0ab76d 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -73,7 +73,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -83,7 +83,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f835e2ef4..c06aff7e1 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -108,7 +108,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -118,7 +118,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 43d5af159..03a32bab8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,7 +40,7 @@ val abstract_operation : compound_rule -> tactic -> tactic val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic val abstract_extended_tactic : - ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic + ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic val refiner : rule -> tactic val frontier : transformation_tactic diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b06ec2f49..c78e842ec 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -306,16 +306,12 @@ type glob_generic_argument = rawconstr_and_expr generic_argument type glob_red_expr = (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen -type closed_raw_generic_argument = constr_expr generic_argument +type typed_generic_argument = Evd.open_constr generic_argument type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type open_generic_argument = Term.constr generic_argument - -type closed_generic_argument = Term.constr generic_argument - -type 'a closed_abstract_argument_type = ('a,Term.constr) abstract_argument_type +type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type type declaration_hook = Decl_kinds.strength -> global_reference -> unit diff --git a/tactics/auto.ml b/tactics/auto.ml index d1caa9862..f0e9842fa 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -216,12 +216,12 @@ let make_apply_entry env sigma (eapply,verbose) (c,cty) = (hd, { pri = nb_hyp cty + nmiss; pat = Some pat; - code = ERes_pf(c,{ce with templenv=empty_env}) }) + code = ERes_pf(c,{ce with env=empty_env}) }) end else (hd, { pri = nb_hyp cty; pat = Some pat; - code = Res_pf(c,{ce with templenv=empty_env}) }) + code = Res_pf(c,{ce with env=empty_env}) }) | _ -> failwith "make_apply_entry" (* eap is (e,v) with e=true if eapply and v=true if verbose @@ -270,7 +270,7 @@ let make_trivial env sigma c = let ce = mk_clenv_from dummy_goal (c,t) in (hd, { pri=1; pat = Some (Pattern.pattern_of_constr (clenv_type ce)); - code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) }) + code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) open Vernacexpr @@ -673,8 +673,11 @@ let gen_trivial lems = function | None -> full_trivial lems | Some l -> trivial lems l +let inj_open c = (Evd.empty,c) + let h_trivial lems l = - Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l) + Refiner.abstract_tactic (TacTrivial (List.map inj_open lems,l)) + (gen_trivial lems l) (**************************************************************************) (* The classical Auto tactic *) @@ -784,7 +787,8 @@ let gen_auto n lems dbnames = let inj_or_var = option_map (fun n -> ArgArg n) let h_auto n lems l = - Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l) + Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l)) + (gen_auto n lems l) (**************************************************************************) (* The "destructing Auto" from Eduardo *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 145411aa1..71817b2c7 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -13,7 +13,8 @@ open Names open Term open Proof_type open Rawterm +open Genarg (*i*) val absurd : constr -> tactic -val contradiction : constr with_bindings option -> tactic +val contradiction : constr with_ebindings option -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml index 90b3c66b2..43ea91f5a 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -136,14 +136,16 @@ let decompose_or c gls = (fun (_,t) -> is_disjunction t) c gls +let inj_open c = (Evd.empty,c) + let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) + Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) + Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) + Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c) (* The tactic Double performs a double induction *) diff --git a/tactics/equality.mli b/tactics/equality.mli index e7726eac3..9254e5f0d 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -26,7 +26,7 @@ open Genarg (*i*) val general_rewrite_bindings : - bool -> constr with_bindings -> evars_flag -> tactic + bool -> constr with_ebindings -> evars_flag -> tactic val general_rewrite : bool -> constr -> tactic @@ -42,16 +42,16 @@ val rewriteRL : constr -> tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) val general_rewrite_bindings_in : - bool -> identifier -> constr with_bindings -> evars_flag -> tactic + bool -> identifier -> constr with_ebindings -> evars_flag -> tactic val general_rewrite_in : bool -> identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : - bool -> evars_flag -> constr with_bindings -> clause -> tactic + bool -> evars_flag -> constr with_ebindings -> clause -> tactic -val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic +val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic val conditional_rewrite_in : - bool -> identifier -> tactic -> constr with_bindings -> tactic + bool -> identifier -> tactic -> constr with_ebindings -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index a1da9d2b3..2f891a61f 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -16,18 +16,18 @@ open Topconstr open Rawterm val rawwit_orient : bool raw_abstract_argument_type -val wit_orient : bool closed_abstract_argument_type +val wit_orient : bool typed_abstract_argument_type val orient : bool Pcoq.Gram.Entry.e val rawwit_morphism_signature : Setoid_replace.morphism_signature raw_abstract_argument_type val wit_morphism_signature : - Setoid_replace.morphism_signature closed_abstract_argument_type + Setoid_replace.morphism_signature typed_abstract_argument_type val morphism_signature : Setoid_replace.morphism_signature Pcoq.Gram.Entry.e val rawwit_raw : constr_expr raw_abstract_argument_type -val wit_raw : rawconstr closed_abstract_argument_type +val wit_raw : rawconstr typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.Entry.e type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -36,20 +36,20 @@ type loc_place = identifier Util.located gen_place type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type -val wit_hloc : place closed_abstract_argument_type +val wit_hloc : place typed_abstract_argument_type val hloc : loc_place Pcoq.Gram.Entry.e val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type -val wit_in_arg_hyp : (Names.identifier list option * bool) closed_abstract_argument_type +val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type -val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type +val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type @@ -57,4 +57,4 @@ val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type -val wit_retroknowledge_field : Retroknowledge.field closed_abstract_argument_type +val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index d51d17aaf..ea33ead5d 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -323,7 +323,7 @@ let step left x tac = let l = List.map (fun lem -> tclTHENLAST - (apply_with_bindings (lem, ImplicitBindings [x])) + (apply_with_bindings (lem, ImplicitBindings [Evd.empty,x])) tac) !(if left then transitivity_left_table else transitivity_right_table) in diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 23d4a275d..341716c01 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -8,17 +8,11 @@ (*i $Id$ i*) -open Util -open Names -open Term open Proof_type open Rawterm -open Tacexpr -open Topconstr -open Genarg val h_discrHyp : quantified_hypothesis -> tactic val h_injHyp : quantified_hypothesis -> tactic -val refine_tac : Genarg.open_constr -> tactic +val refine_tac : Evd.open_constr -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index b8c8e6d18..85a85083e 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -20,6 +20,13 @@ open Tactics open Util let inj_id id = (dummy_loc,id) +let inj_open c = (Evd.empty,c) +let inj_open_wb (c,b) = ((Evd.empty,c),b) +let inj_ia = function + | ElimOnConstr c -> ElimOnConstr (inj_open c) + | ElimOnIdent id -> ElimOnIdent id + | ElimOnAnonHyp n -> ElimOnAnonHyp n +let inj_occ (occ,c) = (occ,inj_open c) (* Basic tactics *) let h_intro_move x y = @@ -27,27 +34,39 @@ let h_intro_move x y = let h_intro x = h_intro_move (Some x) None let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption -let h_exact c = abstract_tactic (TacExact c) (exact_check c) -let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c) +let h_exact c = abstract_tactic (TacExact (inj_open c)) (exact_check c) +let h_exact_no_check c = + abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c) let h_vm_cast_no_check c = - abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) -let h_apply ev cb = abstract_tactic (TacApply (ev,cb)) (apply_with_bindings_gen ev cb) -let h_elim cb cbo = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo) -let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) -let h_case cb = abstract_tactic (TacCase cb) (general_case_analysis cb) -let h_case_type c = abstract_tactic (TacCaseType c) (case_type c) + abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) +let h_apply ev cb = + abstract_tactic (TacApply (ev,inj_open_wb cb)) + (apply_with_bindings_gen ev cb) +let h_elim cb cbo = + abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo)) + (elim cb cbo) +let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) +let h_case cb = abstract_tactic (TacCase (inj_open_wb cb)) (general_case_analysis cb) +let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c) let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) let h_mutual_fix id n l = - abstract_tactic (TacMutualFix (id,n,l)) (mutual_fix id n l) + abstract_tactic + (TacMutualFix (id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l)) + (mutual_fix id n l) let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido) let h_mutual_cofix id l = - abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l) + abstract_tactic + (TacMutualCofix (id,List.map (fun (id,c) -> (id,inj_open c)) l)) + (mutual_cofix id l) -let h_cut c = abstract_tactic (TacCut c) (cut c) -let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl) -let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c) +let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c) +let h_generalize cl = + abstract_tactic (TacGeneralize (List.map inj_open cl)) + (generalize cl) +let h_generalize_dep c = + abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) let h_let_tac na c cl = - abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl) + abstract_tactic (TacLetTac (na,inj_open c,cl)) (letin_tac true na c cl) let h_instantiate n c ido = (Evar_tactics.instantiate n c ido) (* abstract_tactic (TacInstantiate (n,c,cls)) @@ -59,11 +78,13 @@ let h_simple_induction h = let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) let h_new_induction c e idl = - abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl) + abstract_tactic (TacNewInduction (List.map inj_ia c,option_map inj_open_wb e,idl)) + (new_induct c e idl) let h_new_destruct c e idl = - abstract_tactic (TacNewDestruct (c,e,idl)) (new_destruct c e idl) -let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d) -let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) + abstract_tactic (TacNewDestruct (List.map inj_ia c,option_map inj_open_wb e,idl)) + (new_destruct c e idl) +let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) +let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) (* Context management *) let h_clear b l = abstract_tactic (TacClear (b,l)) @@ -89,16 +110,17 @@ let h_simplest_left = h_left NoBindings let h_simplest_right = h_right NoBindings (* Conversion *) -let h_reduce r cl = abstract_tactic (TacReduce (r,cl)) (reduce r cl) +let h_reduce r cl = + abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (oc,c,cl)) + abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl)) (change (option_map Redexpr.out_with_occurrences oc) c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = - abstract_tactic (TacTransitivity c) (intros_transitivity c) + abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c) let h_simplest_apply c = h_apply false (c,NoBindings) let h_simplest_eapply c = h_apply true (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 767f217b9..9c92ddcf2 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -16,6 +16,7 @@ open Tacmach open Genarg open Tacexpr open Rawterm +open Evd (*i*) (* Tactics for the interpreter. They left a trace in the proof tree @@ -32,12 +33,12 @@ val h_exact : constr -> tactic val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic -val h_apply : evars_flag -> constr with_bindings -> tactic +val h_apply : evars_flag -> constr with_ebindings -> tactic -val h_elim : constr with_bindings -> - constr with_bindings option -> tactic +val h_elim : constr with_ebindings -> + constr with_ebindings option -> tactic val h_elim_type : constr -> tactic -val h_case : constr with_bindings -> tactic +val h_case : constr with_ebindings -> tactic val h_case_type : constr -> tactic val h_mutual_fix : identifier -> int -> @@ -58,12 +59,12 @@ val h_instantiate : int -> Rawterm.rawconstr -> val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : - constr induction_arg list -> constr with_bindings option -> + constr induction_arg list -> constr with_ebindings option -> intro_pattern_expr -> tactic val h_new_destruct : - constr induction_arg list -> constr with_bindings option -> + constr induction_arg list -> constr with_ebindings option -> intro_pattern_expr -> tactic -val h_specialize : int option -> constr with_bindings -> tactic +val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic (* Automation tactic : see Auto *) @@ -77,10 +78,10 @@ val h_rename : identifier -> identifier -> tactic (* Constructors *) -val h_constructor : int -> constr bindings -> tactic -val h_left : constr bindings -> tactic -val h_right : constr bindings -> tactic -val h_split : constr bindings -> tactic +val h_constructor : int -> open_constr bindings -> tactic +val h_left : open_constr bindings -> tactic +val h_right : open_constr bindings -> tactic +val h_split : open_constr bindings -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index b799c939f..47b8ca64b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -47,7 +47,7 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then let metas = List.filter (fun na -> na<>Anonymous) - (List.map (Evd.meta_name clenv.env) (collect_meta_variables ccl)) in + (List.map (Evd.meta_name clenv.evd) (collect_meta_variables ccl)) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a0ff76968..1b308e298 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -292,7 +292,7 @@ let add_inversion_lemma_exn na com comsort bool tac = let lemInv id c gls = try let clause = mk_clenv_type_of gls c in - let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in + let clause = clenv_constrain_with_bindings [(-1,(Evd.empty,mkVar id))] clause in Clenvtac.res_pf clause ~allow_K:true gls with | UserError (a,b) -> diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 170f2948d..8fc95b408 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1734,14 +1734,14 @@ let unification_rewrite c1 c2 cl but gl = (* ~mod_delta:false to allow to mark occurences that must not be rewritten simply by replacing them with let-defined definitions in the context *) - w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env + w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.evd with Pretype_errors.PretypeError _ -> (* ~mod_delta:true to make Ring work (since it really exploits conversion) *) - w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env + w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.evd in - let cl' = {cl with env = env' } in + let cl' = {cl with evd = env' } in let c2 = Clenv.clenv_nf_meta cl' c2 in check_evar_map_of_evars_defs env' ; env',Clenv.clenv_value cl', c1, c2 @@ -1983,7 +1983,7 @@ let setoid_transitivity c gl = | _ -> assert false in apply_with_bindings - (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl + (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, (Evd.empty,c) ]) gl with Optimize -> transitivity c gl ;; diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4dfcebbe7..aba013c1c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -288,7 +288,7 @@ type glob_sign = { type interp_genarg_type = (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> - closed_generic_argument) * + typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) let extragenargtab = @@ -1367,6 +1367,21 @@ let pf_interp_constr_list_as_list ist gl (c,_ as x) = let pf_interp_constr_list ist gl l = List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l) +let inj_open c = (Evd.empty,c) + +let pf_interp_open_constr_list_as_list ist gl (c,_ as x) = + match c with + | RVar (_,id) -> + (try List.map inj_open + (constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)) + with Not_found -> + [interp_open_constr None ist (project gl) (pf_env gl) x]) + | _ -> + [interp_open_constr None ist (project gl) (pf_env gl) x] + +let pf_interp_open_constr_list ist gl l = + List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l) + (* Interprets a type expression *) let pf_interp_type ist gl = interp_type ist (project gl) (pf_env gl) @@ -1446,6 +1461,12 @@ let interp_constr_may_eval ist gl c = csr end +let inj_may_eval = function + | ConstrTerm c -> ConstrTerm (inj_open c) + | ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c) + | ConstrContext (id,c) -> ConstrContext (id,inj_open c) + | ConstrTypeOf c -> ConstrTypeOf (inj_open c) + let message_of_value = function | VVoid -> str "()" | VInteger n -> int n @@ -1517,16 +1538,19 @@ let interp_induction_arg ist gl = function (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id))))) let interp_binding ist gl (loc,b,c) = - (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c) + (loc,interp_quantified_hypothesis ist b,pf_interp_open_constr false ist gl c) let interp_bindings ist gl = function | NoBindings -> NoBindings -| ImplicitBindings l -> ImplicitBindings (pf_interp_constr_list ist gl l) +| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l) | ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l) let interp_constr_with_bindings ist gl (c,bl) = (pf_interp_constr ist gl c, interp_bindings ist gl bl) +let interp_open_constr_with_bindings ist gl (c,bl) = + (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl) + let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c) let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) @@ -2047,7 +2071,7 @@ and interp_atomic ist gl = function | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in - abstract_tactic (TacAssert (t,ipat,c)) + abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (option_map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ca9b076d9..b4a715983 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -66,11 +66,11 @@ val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) val add_tactic : - string -> (closed_generic_argument list -> tactic) -> unit + string -> (typed_generic_argument list -> tactic) -> unit val overwriting_add_tactic : - string -> (closed_generic_argument list -> tactic) -> unit + string -> (typed_generic_argument list -> tactic) -> unit val lookup_tactic : - string -> (closed_generic_argument list) -> tactic + string -> (typed_generic_argument list) -> tactic (* Adds an interpretation function for extra generic arguments *) type glob_sign = { @@ -83,12 +83,12 @@ val add_interp_genarg : string -> (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> - closed_generic_argument) * + typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) -> unit val interp_genarg : - interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument + interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e71911f6b..b042a8422 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -505,7 +505,7 @@ let cut_in_parallel l = prec (List.rev l) let error_uninstantiated_metas t clenv = - let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in + let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id) @@ -516,7 +516,7 @@ let clenv_refine_in with_evars id clenv gl = error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in tclTHEN - (tclEVARS (evars_of clenv.env)) + (tclEVARS (evars_of clenv.evd)) (cut_replacing id new_hyp_typ (fun x gl -> refine_no_check new_hyp_prf gl)) gl @@ -558,8 +558,19 @@ let eapply_with_bindings = apply_with_bindings_gen true let apply c = apply_with_bindings (c,NoBindings) +let inj_open c = (Evd.empty,c) + +let inj_occ (occ,c) = (occ,inj_open c) + +let inj_red_expr = function + | Simpl lo -> Simpl (option_map inj_occ lo) + | Fold l -> Fold (List.map inj_open l) + | Pattern l -> Pattern (List.map inj_occ l) + | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c) + -> c + let apply_list = function - | c::l -> apply_with_bindings (c,ImplicitBindings l) + | c::l -> apply_with_bindings (c,ImplicitBindings (List.map inj_open l)) | _ -> assert false (* Resolution with no reduction on the type *) @@ -710,7 +721,7 @@ let new_hyp mopt (c,lbind) g = | Some m -> if m < nargs then list_firstn m tstack else tstack | None -> tstack) in - (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env)) + (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd)) (cut (pf_type_of g cut_pf))) ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g @@ -1530,7 +1541,7 @@ let cook_sign hyp0_opt indvars_init env = (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: (Term.constr * constr Rawterm.bindings) option; + elimc: constr with_ebindings option; elimt: types; indref: global_reference option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 52c5ba883..6b0f8413a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -28,12 +28,15 @@ open Nametab open Rawterm (*i*) +val inj_open : constr -> open_constr +val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen + (* Main tactics. *) (*s General functions. *) val type_clenv_binding : goal sigma -> - constr * constr -> constr bindings -> constr + constr * constr -> open_constr bindings -> constr val string_of_inductive : constr -> string val head_constr : constr -> constr list @@ -152,7 +155,7 @@ val clear : identifier list -> tactic val clear_body : identifier list -> tactic val keep : identifier list -> tactic -val new_hyp : int option -> constr with_bindings -> tactic +val new_hyp : int option -> constr with_ebindings -> tactic val move_hyp : bool -> identifier -> identifier -> tactic val rename_hyp : identifier -> identifier -> tactic @@ -166,13 +169,13 @@ val bring_hyps : named_context -> tactic val apply : constr -> tactic val apply_without_reduce : constr -> tactic val apply_list : constr list -> tactic -val apply_with_bindings_gen : evars_flag -> constr with_bindings -> tactic -val apply_with_bindings : constr with_bindings -> tactic -val eapply_with_bindings : constr with_bindings -> tactic +val apply_with_bindings_gen : evars_flag -> constr with_ebindings -> tactic +val apply_with_bindings : constr with_ebindings -> tactic +val eapply_with_bindings : constr with_ebindings -> tactic val cut_and_apply : constr -> tactic -val apply_in : evars_flag -> identifier -> constr with_bindings list -> tactic +val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic (*s Elimination tactics. *) @@ -203,7 +206,7 @@ val apply_in : evars_flag -> identifier -> constr with_bindings list -> tactic (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: (Term.constr * constr Rawterm.bindings) option; + elimc: constr with_ebindings option; elimt: types; indref: global_reference option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) @@ -223,28 +226,28 @@ type elim_scheme = { } -val compute_elim_sig : ?elimc: (Term.constr * constr Rawterm.bindings) -> types -> elim_scheme +val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme val general_elim : - constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic + constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic val general_elim_in : evars_flag -> - identifier -> constr with_bindings -> constr with_bindings -> tactic + identifier -> constr with_ebindings -> constr with_ebindings -> tactic -val default_elim : constr with_bindings -> tactic +val default_elim : constr with_ebindings -> tactic val simplest_elim : constr -> tactic -val elim : constr with_bindings -> constr with_bindings option -> tactic +val elim : constr with_ebindings -> constr with_ebindings option -> tactic val simple_induct : quantified_hypothesis -> tactic -val new_induct : constr induction_arg list -> constr with_bindings option -> +val new_induct : constr induction_arg list -> constr with_ebindings option -> intro_pattern_expr -> tactic (*s Case analysis tactics. *) -val general_case_analysis : constr with_bindings -> tactic +val general_case_analysis : constr with_ebindings -> tactic val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : constr induction_arg list -> constr with_bindings option -> +val new_destruct : constr induction_arg list -> constr with_ebindings option -> intro_pattern_expr -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -265,14 +268,14 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) val constructor_tac : int option -> int -> - constr bindings -> tactic -val one_constructor : int -> constr bindings -> tactic + open_constr bindings -> tactic +val one_constructor : int -> open_constr bindings -> tactic val any_constructor : tactic option -> tactic -val left : constr bindings -> tactic +val left : open_constr bindings -> tactic val simplest_left : tactic -val right : constr bindings -> tactic +val right : open_constr bindings -> tactic val simplest_right : tactic -val split : constr bindings -> tactic +val split : open_constr bindings -> tactic val simplest_split : tactic (*s Logical connective tactics. *) |