diff options
56 files changed, 1525 insertions, 1344 deletions
@@ -46,10 +46,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/univ.cmi kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi -kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi +kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi @@ -69,9 +69,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/bignat.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/compat.cmo lib/pp.cmi library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \ @@ -100,6 +97,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \ library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/compat.cmo lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \ lib/util.cmi @@ -170,8 +170,6 @@ pretyping/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/term.cmi pretyping/inductiveops.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi -pretyping/instantiate.cmi: kernel/environ.cmi pretyping/evd.cmi \ - kernel/names.cmi kernel/sign.cmi kernel/term.cmi pretyping/matching.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/pattern.cmi kernel/term.cmi pretyping/termops.cmi pretyping/pattern.cmi: kernel/environ.cmi library/libnames.cmi \ @@ -200,10 +198,15 @@ pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \ pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi -proofs/clenv.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ - lib/pp.cmi pretyping/pretyping.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/termops.cmi lib/util.cmi +pretyping/unification.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ + pretyping/evd.cmi kernel/names.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi kernel/term.cmi lib/util.cmi +proofs/clenv.cmi: pretyping/evd.cmi kernel/names.cmi lib/pp.cmi \ + pretyping/pretyping.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi +proofs/clenvtac.cmi: proofs/clenv.cmi pretyping/evd.cmi kernel/names.cmi \ + proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi interp/topconstr.cmi @@ -228,9 +231,9 @@ proofs/tacmach.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ kernel/sign.cmi proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ pretyping/termops.cmi interp/topconstr.cmi -proofs/tactic_debug.cmi: kernel/environ.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo \ - kernel/term.cmi +proofs/tactic_debug.cmi: kernel/environ.cmi pretyping/evd.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ + proofs/tacexpr.cmo kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/environ.cmi \ pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ @@ -321,11 +324,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi -toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \ parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \ @@ -345,9 +348,9 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi contrib/correctness/past.cmi: kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi lib/util.cmi -contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi +contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi contrib/correctness/penv.cmi: library/libnames.cmi kernel/names.cmi \ @@ -410,16 +413,15 @@ contrib/funind/tacinvutils.cmi: interp/coqlib.cmi tactics/equality.cmi \ tactics/refine.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi -contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ - proofs/tacmach.cmi +contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo contrib/interface/dad.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi interp/topconstr.cmi -contrib/interface/debug_tac.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ - proofs/tacmach.cmi +contrib/interface/debug_tac.cmi: pretyping/evd.cmi proofs/proof_type.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi contrib/interface/name_to_ast.cmi: parsing/coqast.cmi library/libnames.cmi \ toplevel/vernacexpr.cmo contrib/interface/pbp.cmi: kernel/names.cmi proofs/proof_type.cmi \ - proofs/tacexpr.cmo proofs/tacmach.cmi + proofs/tacexpr.cmo contrib/interface/showproof.cmi: contrib/interface/ascent.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi kernel/inductive.cmi \ @@ -476,6 +478,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi ide/config_lexer.cmx: ide/config_parser.cmx lib/util.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: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \ + ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \ + ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \ + ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi +ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \ + ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \ + ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \ + ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \ kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \ @@ -498,14 +508,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \ toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi -ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \ - ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \ - ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \ - ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi -ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \ - ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \ - ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \ - ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -658,6 +660,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi +kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/modops.cmi +kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ + kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ @@ -666,12 +674,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi -kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/modops.cmi -kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \ lib/predicate.cmi lib/util.cmi kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \ @@ -752,10 +754,10 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.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/gmap.cmi lib/util.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/gmap.cmx lib/util.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 @@ -764,24 +766,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/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/compat.cmo lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ @@ -888,6 +880,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ lib/system.cmx library/states.cmi library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/compat.cmo lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -1124,24 +1126,22 @@ parsing/prettyp.cmo: pretyping/classops.cmi interp/constrextern.cmi \ kernel/conv_oracle.cmi kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ library/impargs.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - pretyping/instantiate.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \ - parsing/printmod.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi interp/symbols.cmi \ - interp/syntax_def.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - parsing/prettyp.cmi + library/lib.cmi library/libnames.cmi library/libobject.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi parsing/printer.cmi parsing/printmod.cmi kernel/reduction.cmi \ + pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + interp/symbols.cmi interp/syntax_def.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi parsing/prettyp.cmi parsing/prettyp.cmx: pretyping/classops.cmx interp/constrextern.cmx \ kernel/conv_oracle.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ library/impargs.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - pretyping/instantiate.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ - parsing/printmod.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx interp/symbols.cmx \ - interp/syntax_def.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - parsing/prettyp.cmi + library/lib.cmx library/libnames.cmx library/libobject.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx parsing/printer.cmx parsing/printmod.cmx kernel/reduction.cmx \ + pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + interp/symbols.cmx interp/syntax_def.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi parsing/printer.cmo: parsing/ast.cmi interp/constrextern.cmi \ parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \ parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \ @@ -1239,11 +1239,11 @@ pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \ kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \ kernel/typeops.cmx lib/util.cmx pretyping/cases.cmi pretyping/cbv.cmo: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \ - pretyping/evd.cmi pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi \ - kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi + pretyping/evd.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi pretyping/cbv.cmx: kernel/closure.cmx kernel/environ.cmx kernel/esubst.cmx \ - pretyping/evd.cmx pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \ - kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi + pretyping/evd.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi pretyping/classops.cmo: library/decl_kinds.cmo kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi lib/gmap.cmi library/goptions.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ @@ -1282,48 +1282,46 @@ pretyping/detyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ pretyping/termops.cmx kernel/univ.cmx lib/util.cmx pretyping/detyping.cmi pretyping/evarconv.cmo: pretyping/classops.cmi kernel/closure.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ - pretyping/instantiate.cmi library/libnames.cmi kernel/names.cmi \ - pretyping/rawterm.cmi pretyping/recordops.cmi pretyping/reductionops.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi + library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ + pretyping/recordops.cmi pretyping/reductionops.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi pretyping/evarconv.cmx: pretyping/classops.cmx kernel/closure.cmx \ kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ - pretyping/instantiate.cmx library/libnames.cmx kernel/names.cmx \ - pretyping/rawterm.cmx pretyping/recordops.cmx pretyping/reductionops.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi + library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ + pretyping/recordops.cmx pretyping/reductionops.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi pretyping/evarutil.cmo: kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi pretyping/indrec.cmi pretyping/instantiate.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi \ - pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \ - pretyping/evarutil.cmi + library/global.cmi pretyping/indrec.cmi library/nameops.cmi \ + kernel/names.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi kernel/univ.cmi \ + lib/util.cmi pretyping/evarutil.cmi pretyping/evarutil.cmx: kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx pretyping/indrec.cmx pretyping/instantiate.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmx \ - pretyping/reductionops.cmx kernel/sign.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ - pretyping/evarutil.cmi -pretyping/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - lib/util.cmi pretyping/evd.cmi -pretyping/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \ - lib/util.cmx pretyping/evd.cmi + library/global.cmx pretyping/indrec.cmx library/nameops.cmx \ + kernel/names.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/rawterm.cmx pretyping/reductionops.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx kernel/univ.cmx \ + lib/util.cmx pretyping/evarutil.cmi +pretyping/evd.cmo: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ + kernel/term.cmi lib/util.cmi pretyping/evd.cmi +pretyping/evd.cmx: kernel/environ.cmx kernel/names.cmx kernel/sign.cmx \ + kernel/term.cmx lib/util.cmx pretyping/evd.cmi pretyping/indrec.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi library/global.cmi kernel/indtypes.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi kernel/reduction.cmi \ - pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \ - lib/util.cmi pretyping/indrec.cmi + kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + kernel/safe_typing.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ + pretyping/indrec.cmi pretyping/indrec.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx library/global.cmx kernel/indtypes.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx kernel/reduction.cmx \ - pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ - lib/util.cmx pretyping/indrec.cmi + kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + kernel/safe_typing.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ + pretyping/indrec.cmi pretyping/inductiveops.cmo: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ kernel/names.cmi pretyping/reductionops.cmi kernel/sign.cmi \ @@ -1334,12 +1332,6 @@ pretyping/inductiveops.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx pretyping/reductionops.cmx kernel/sign.cmx \ kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \ pretyping/inductiveops.cmi -pretyping/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ - kernel/term.cmi lib/util.cmi pretyping/instantiate.cmi -pretyping/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \ - pretyping/evd.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ - kernel/term.cmx lib/util.cmx pretyping/instantiate.cmi pretyping/matching.cmo: kernel/environ.cmi library/libnames.cmi \ library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/term.cmi \ @@ -1357,39 +1349,37 @@ pretyping/pattern.cmx: kernel/environ.cmx library/libnames.cmx \ lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ pretyping/pattern.cmi pretyping/pretype_errors.cmo: kernel/environ.cmi pretyping/evd.cmi \ - pretyping/inductiveops.cmi kernel/names.cmi pretyping/rawterm.cmi \ - kernel/reduction.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ - pretyping/pretype_errors.cmi + pretyping/inductiveops.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/type_errors.cmi lib/util.cmi pretyping/pretype_errors.cmi pretyping/pretype_errors.cmx: kernel/environ.cmx pretyping/evd.cmx \ - pretyping/inductiveops.cmx kernel/names.cmx pretyping/rawterm.cmx \ - kernel/reduction.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ - pretyping/pretype_errors.cmi + pretyping/inductiveops.cmx kernel/names.cmx library/nametab.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/type_errors.cmx lib/util.cmx pretyping/pretype_errors.cmi pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \ pretyping/coercion.cmi kernel/declarations.cmi pretyping/detyping.cmi \ lib/dyn.cmi kernel/environ.cmi pretyping/evarconv.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - pretyping/instantiate.cmi library/libnames.cmi library/nameops.cmi \ - kernel/names.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi \ - pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ - pretyping/pretyping.cmi + library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/rawterm.cmi pretyping/recordops.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \ + pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \ + lib/util.cmi pretyping/pretyping.cmi pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \ pretyping/coercion.cmx kernel/declarations.cmx pretyping/detyping.cmx \ lib/dyn.cmx kernel/environ.cmx pretyping/evarconv.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - pretyping/instantiate.cmx library/libnames.cmx library/nameops.cmx \ - kernel/names.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmx \ - pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ - pretyping/pretyping.cmi + library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/rawterm.cmx pretyping/recordops.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ + pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ + lib/util.cmx pretyping/pretyping.cmi pretyping/rawterm.cmo: lib/dyn.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \ lib/util.cmi pretyping/rawterm.cmi @@ -1407,37 +1397,35 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \ kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/recordops.cmi pretyping/reductionops.cmo: kernel/closure.cmi kernel/declarations.cmi \ - kernel/environ.cmi kernel/esubst.cmi pretyping/evd.cmi \ - pretyping/instantiate.cmi kernel/names.cmi lib/pp.cmi \ - kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/environ.cmi kernel/esubst.cmi pretyping/evd.cmi kernel/names.cmi \ + lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \ pretyping/reductionops.cmi pretyping/reductionops.cmx: kernel/closure.cmx kernel/declarations.cmx \ - kernel/environ.cmx kernel/esubst.cmx pretyping/evd.cmx \ - pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \ - kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/environ.cmx kernel/esubst.cmx pretyping/evd.cmx kernel/names.cmx \ + lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \ pretyping/reductionops.cmi pretyping/retyping.cmo: kernel/declarations.cmi kernel/environ.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ + pretyping/evd.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ kernel/names.cmi pretyping/reductionops.cmi kernel/term.cmi \ kernel/typeops.cmi kernel/univ.cmi lib/util.cmi pretyping/retyping.cmi pretyping/retyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ + pretyping/evd.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ kernel/names.cmx pretyping/reductionops.cmx kernel/term.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx pretyping/retyping.cmi pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \ kernel/conv_oracle.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ - pretyping/instantiate.cmi library/libnames.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ + library/libnames.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/tacred.cmi pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \ kernel/conv_oracle.cmx kernel/declarations.cmx kernel/environ.cmx \ pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ - pretyping/instantiate.cmx library/libnames.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ + library/libnames.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \ kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/tacred.cmi pretyping/termops.cmo: kernel/environ.cmi library/global.cmi library/lib.cmi \ @@ -1448,50 +1436,80 @@ pretyping/termops.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \ library/libnames.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ kernel/univ.cmx lib/util.cmx pretyping/termops.cmi -pretyping/typing.cmo: kernel/environ.cmi kernel/inductive.cmi \ - pretyping/instantiate.cmi kernel/names.cmi pretyping/pretype_errors.cmi \ - pretyping/reductionops.cmi kernel/term.cmi kernel/type_errors.cmi \ - kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi -pretyping/typing.cmx: kernel/environ.cmx kernel/inductive.cmx \ - pretyping/instantiate.cmx kernel/names.cmx pretyping/pretype_errors.cmx \ - pretyping/reductionops.cmx kernel/term.cmx kernel/type_errors.cmx \ - kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi +pretyping/typing.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ + pretyping/evd.cmi kernel/inductive.cmi kernel/names.cmi \ + pretyping/pretype_errors.cmi pretyping/reductionops.cmi kernel/term.cmi \ + kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ + pretyping/typing.cmi +pretyping/typing.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ + pretyping/evd.cmx kernel/inductive.cmx kernel/names.cmx \ + pretyping/pretype_errors.cmx pretyping/reductionops.cmx kernel/term.cmx \ + kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ + pretyping/typing.cmi +pretyping/unification.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ + pretyping/evd.cmi library/nameops.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + pretyping/unification.cmi +pretyping/unification.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ + pretyping/evd.cmx library/nameops.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/rawterm.cmx pretyping/reductionops.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + pretyping/unification.cmi proofs/clenv.cmo: pretyping/coercion.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ - library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi \ - library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + library/global.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ pretyping/retyping.cmi kernel/sign.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi + pretyping/unification.cmi lib/util.cmi proofs/clenv.cmi proofs/clenv.cmx: pretyping/coercion.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ - library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx \ - library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + library/global.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ pretyping/retyping.cmx kernel/sign.cmx proofs/tacexpr.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi + pretyping/unification.cmx lib/util.cmx proofs/clenv.cmi +proofs/clenvtac.cmo: proofs/clenv.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ + proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/unification.cmi \ + lib/util.cmi proofs/clenvtac.cmi +proofs/clenvtac.cmx: proofs/clenv.cmx kernel/environ.cmx \ + proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ + proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/unification.cmx \ + lib/util.cmx proofs/clenvtac.cmi proofs/evar_refiner.cmo: interp/constrintern.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ - pretyping/instantiate.cmi proofs/logic.cmi library/nameops.cmi \ - kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/pretyping.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/type_errors.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/evar_refiner.cmi + proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + lib/pp.cmi pretyping/pretyping.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/type_errors.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/evar_refiner.cmi proofs/evar_refiner.cmx: interp/constrintern.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ - pretyping/instantiate.cmx proofs/logic.cmx library/nameops.cmx \ - kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/pretyping.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/type_errors.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/evar_refiner.cmi + proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + lib/pp.cmx pretyping/pretyping.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/type_errors.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/evar_refiner.cmi proofs/logic.cmo: interp/constrextern.cmi parsing/coqast.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ @@ -1547,19 +1565,19 @@ proofs/proof_type.cmx: kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx \ pretyping/pattern.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ kernel/term.cmx lib/util.cmx proofs/proof_type.cmi proofs/refiner.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ - proofs/logic.cmi lib/options.cmi lib/pp.cmi parsing/pptactic.cmi \ - translate/pptacticnew.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi + pretyping/evd.cmi library/global.cmi proofs/logic.cmi lib/options.cmi \ + lib/pp.cmi parsing/pptactic.cmi translate/pptacticnew.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/reductionops.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ + proofs/refiner.cmi proofs/refiner.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \ - proofs/logic.cmx lib/options.cmx lib/pp.cmx parsing/pptactic.cmx \ - translate/pptacticnew.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi + pretyping/evd.cmx library/global.cmx proofs/logic.cmx lib/options.cmx \ + lib/pp.cmx parsing/pptactic.cmx translate/pptacticnew.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/reductionops.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ + proofs/refiner.cmi proofs/tacexpr.cmo: library/decl_kinds.cmo lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi pretyping/rawterm.cmi kernel/term.cmi \ @@ -1569,21 +1587,19 @@ proofs/tacexpr.cmx: library/decl_kinds.cmx lib/dyn.cmx interp/genarg.cmx \ pretyping/pattern.cmx pretyping/rawterm.cmx kernel/term.cmx \ interp/topconstr.cmx lib/util.cmx proofs/tacmach.cmo: interp/constrintern.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ - kernel/sign.cmi proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/tacmach.cmi + pretyping/evd.cmi library/global.cmi proofs/logic.cmi library/nameops.cmi \ + kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi proofs/tacmach.cmx: interp/constrintern.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ - kernel/sign.cmx proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/tacmach.cmi + pretyping/evd.cmx library/global.cmx proofs/logic.cmx library/nameops.cmx \ + kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi proofs/tactic_debug.cmo: parsing/ast.cmi interp/constrextern.cmi \ library/global.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \ lib/pp.cmi parsing/pptactic.cmi translate/pptacticnew.cmi \ @@ -1671,25 +1687,27 @@ tactics/dhyp.cmx: parsing/ast.cmx proofs/clenv.cmx interp/constrintern.cmx \ tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi tactics/eauto.cmo: tactics/auto.cmi toplevel/cerrors.cmi proofs/clenv.cmi \ - kernel/declarations.cmi parsing/egrammar.cmi proofs/evar_refiner.cmi \ - lib/explore.cmi parsing/extend.cmi interp/genarg.cmi library/global.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi tactics/eauto.cmi + proofs/clenvtac.cmi kernel/declarations.cmi parsing/egrammar.cmi \ + proofs/evar_refiner.cmi lib/explore.cmi parsing/extend.cmi \ + interp/genarg.cmi library/global.cmi proofs/logic.cmi library/nameops.cmi \ + kernel/names.cmi lib/options.cmi pretyping/pattern.cmi parsing/pcoq.cmi \ + lib/pp.cmi parsing/pptactic.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + tactics/eauto.cmi tactics/eauto.cmx: tactics/auto.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ - kernel/declarations.cmx parsing/egrammar.cmx proofs/evar_refiner.cmx \ - lib/explore.cmx parsing/extend.cmx interp/genarg.cmx library/global.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - pretyping/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx tactics/eauto.cmi + proofs/clenvtac.cmx kernel/declarations.cmx parsing/egrammar.cmx \ + proofs/evar_refiner.cmx lib/explore.cmx parsing/extend.cmx \ + interp/genarg.cmx library/global.cmx proofs/logic.cmx library/nameops.cmx \ + kernel/names.cmx lib/options.cmx pretyping/pattern.cmx parsing/pcoq.cmx \ + lib/pp.cmx parsing/pptactic.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ + tactics/eauto.cmi tactics/elim.cmo: proofs/clenv.cmi kernel/environ.cmi interp/genarg.cmi \ tactics/hiddentac.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ @@ -1726,9 +1744,9 @@ tactics/eqdecide.cmx: tactics/auto.cmx toplevel/cerrors.cmx interp/coqlib.cmx \ kernel/term.cmx lib/util.cmx tactics/equality.cmo: proofs/clenv.cmi interp/coqlib.cmi \ kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ - pretyping/evarconv.cmi pretyping/evarutil.cmi tactics/hipattern.cmi \ - pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - pretyping/instantiate.cmi library/libnames.cmi proofs/logic.cmi \ + pretyping/evarconv.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ + tactics/hipattern.cmi pretyping/indrec.cmi kernel/inductive.cmi \ + pretyping/inductiveops.cmi library/libnames.cmi proofs/logic.cmi \ pretyping/matching.cmi library/nameops.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ @@ -1739,9 +1757,9 @@ tactics/equality.cmo: proofs/clenv.cmi interp/coqlib.cmi \ toplevel/vernacexpr.cmo tactics/equality.cmi tactics/equality.cmx: proofs/clenv.cmx interp/coqlib.cmx \ kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ - pretyping/evarconv.cmx pretyping/evarutil.cmx tactics/hipattern.cmx \ - pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - pretyping/instantiate.cmx library/libnames.cmx proofs/logic.cmx \ + pretyping/evarconv.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ + tactics/hipattern.cmx pretyping/indrec.cmx kernel/inductive.cmx \ + pretyping/inductiveops.cmx library/libnames.cmx proofs/logic.cmx \ pretyping/matching.cmx library/nameops.cmx kernel/names.cmx \ pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ @@ -1818,46 +1836,48 @@ tactics/hipattern.cmx: proofs/clenv.cmx interp/coqlib.cmx \ tactics/hipattern.cmi tactics/inv.cmo: proofs/clenv.cmi interp/coqlib.cmi tactics/elim.cmi \ kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \ - interp/genarg.cmi library/global.cmi tactics/hipattern.cmi \ - pretyping/inductiveops.cmi pretyping/matching.cmi library/nameops.cmi \ - kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi tactics/inv.cmi + pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ + tactics/hipattern.cmi pretyping/inductiveops.cmi pretyping/matching.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ + kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi pretyping/typing.cmi pretyping/unification.cmi \ + lib/util.cmi tactics/inv.cmi tactics/inv.cmx: proofs/clenv.cmx interp/coqlib.cmx tactics/elim.cmx \ kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \ - interp/genarg.cmx library/global.cmx tactics/hipattern.cmx \ - pretyping/inductiveops.cmx pretyping/matching.cmx library/nameops.cmx \ - kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx tactics/inv.cmi -tactics/leminv.cmo: proofs/clenv.cmi interp/constrintern.cmi \ - library/decl_kinds.cmo kernel/declarations.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ - pretyping/evd.cmi library/global.cmi pretyping/inductiveops.cmi \ - tactics/inv.cmi library/nameops.cmi kernel/names.cmi proofs/pfedit.cmi \ - lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacexpr.cmo \ - tactics/leminv.cmi -tactics/leminv.cmx: proofs/clenv.cmx interp/constrintern.cmx \ - library/decl_kinds.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ - pretyping/evd.cmx library/global.cmx pretyping/inductiveops.cmx \ - tactics/inv.cmx library/nameops.cmx kernel/names.cmx proofs/pfedit.cmx \ - lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx \ + pretyping/evd.cmx interp/genarg.cmx library/global.cmx \ + tactics/hipattern.cmx pretyping/inductiveops.cmx pretyping/matching.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ + kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - tactics/leminv.cmi + pretyping/termops.cmx pretyping/typing.cmx pretyping/unification.cmx \ + lib/util.cmx tactics/inv.cmi +tactics/leminv.cmo: proofs/clenv.cmi proofs/clenvtac.cmi \ + interp/constrintern.cmi library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ + pretyping/inductiveops.cmi tactics/inv.cmi library/nameops.cmi \ + kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi pretyping/pretyping.cmi \ + parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo tactics/leminv.cmi +tactics/leminv.cmx: proofs/clenv.cmx proofs/clenvtac.cmx \ + interp/constrintern.cmx library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ + proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ + pretyping/inductiveops.cmx tactics/inv.cmx library/nameops.cmx \ + kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx pretyping/pretyping.cmx \ + parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx tactics/leminv.cmi tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi pretyping/pattern.cmi \ kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi @@ -1876,24 +1896,26 @@ tactics/refine.cmx: proofs/clenv.cmx kernel/environ.cmx pretyping/evd.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ tactics/refine.cmi -tactics/setoid_replace.cmo: tactics/auto.cmi interp/constrintern.cmi \ +tactics/setoid_replace.cmo: proofs/clenv.cmi interp/constrintern.cmi \ interp/coqlib.cmi library/decl_kinds.cmo library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi lib/gmap.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ + kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ + pretyping/evd.cmi library/global.cmi lib/gmap.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ + lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ kernel/safe_typing.cmi library/summary.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacexpr.cmo tactics/setoid_replace.cmi -tactics/setoid_replace.cmx: tactics/auto.cmx interp/constrintern.cmx \ +tactics/setoid_replace.cmx: proofs/clenv.cmx interp/constrintern.cmx \ interp/coqlib.cmx library/decl_kinds.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx lib/gmap.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ + kernel/entries.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ + pretyping/evd.cmx library/global.cmx lib/gmap.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ + lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ kernel/safe_typing.cmx library/summary.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ @@ -1932,40 +1954,44 @@ tactics/tacinterp.cmx: parsing/ast.cmx tactics/auto.cmx kernel/closure.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ tactics/tacinterp.cmi -tactics/tacticals.cmo: proofs/clenv.cmi kernel/declarations.cmi \ - kernel/environ.cmi proofs/evar_refiner.cmi interp/genarg.cmi \ - library/global.cmi pretyping/indrec.cmi kernel/inductive.cmi \ - library/libnames.cmi pretyping/matching.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \ +tactics/tacticals.cmo: proofs/clenv.cmi proofs/clenvtac.cmi \ + kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ + pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ + pretyping/indrec.cmi kernel/inductive.cmi library/libnames.cmi \ + pretyping/matching.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi tactics/tacticals.cmi -tactics/tacticals.cmx: proofs/clenv.cmx kernel/declarations.cmx \ - kernel/environ.cmx proofs/evar_refiner.cmx interp/genarg.cmx \ - library/global.cmx pretyping/indrec.cmx kernel/inductive.cmx \ - library/libnames.cmx pretyping/matching.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx kernel/reduction.cmx proofs/refiner.cmx \ - kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.cmx \ +tactics/tacticals.cmx: proofs/clenv.cmx proofs/clenvtac.cmx \ + kernel/declarations.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ + pretyping/evd.cmx interp/genarg.cmx library/global.cmx \ + pretyping/indrec.cmx kernel/inductive.cmx library/libnames.cmx \ + pretyping/matching.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx tactics/tacticals.cmi -tactics/tactics.cmo: proofs/clenv.cmi interp/constrintern.cmi \ - interp/coqlib.cmi library/decl_kinds.cmo kernel/declarations.cmi \ - library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi pretyping/evd.cmi interp/genarg.cmi \ - library/global.cmi tactics/hipattern.cmi pretyping/indrec.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \ +tactics/tactics.cmo: proofs/clenv.cmi proofs/clenvtac.cmi \ + interp/constrintern.cmi interp/coqlib.cmi library/decl_kinds.cmo \ + kernel/declarations.cmi library/declare.cmi kernel/entries.cmi \ + kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ + interp/genarg.cmi library/global.cmi tactics/hipattern.cmi \ + pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ + library/libnames.cmi proofs/logic.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ + lib/pp.cmi pretyping/pretype_errors.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi -tactics/tactics.cmx: proofs/clenv.cmx interp/constrintern.cmx \ - interp/coqlib.cmx library/decl_kinds.cmx kernel/declarations.cmx \ - library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ - proofs/evar_refiner.cmx pretyping/evd.cmx interp/genarg.cmx \ - library/global.cmx tactics/hipattern.cmx pretyping/indrec.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ - lib/options.cmx proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx \ +tactics/tactics.cmx: proofs/clenv.cmx proofs/clenvtac.cmx \ + interp/constrintern.cmx interp/coqlib.cmx library/decl_kinds.cmx \ + kernel/declarations.cmx library/declare.cmx kernel/entries.cmx \ + kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ + interp/genarg.cmx library/global.cmx tactics/hipattern.cmx \ + pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ + library/libnames.cmx proofs/logic.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ + lib/pp.cmx pretyping/pretype_errors.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx \ @@ -2080,24 +2106,22 @@ toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ kernel/cooking.cmi library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/environ.cmi library/global.cmi library/impargs.cmi \ - kernel/indtypes.cmi kernel/inductive.cmi pretyping/instantiate.cmi \ - library/lib.cmi library/libnames.cmi library/libobject.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi toplevel/recordobj.cmi \ - pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \ - library/summary.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi toplevel/discharge.cmi + kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi library/library.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + lib/pp.cmi toplevel/recordobj.cmi pretyping/recordops.cmi \ + kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \ + kernel/typeops.cmi kernel/univ.cmi lib/util.cmi toplevel/discharge.cmi toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ kernel/cooking.cmx library/decl_kinds.cmx kernel/declarations.cmx \ library/declare.cmx library/dischargedhypsmap.cmx kernel/entries.cmx \ kernel/environ.cmx library/global.cmx library/impargs.cmx \ - kernel/indtypes.cmx kernel/inductive.cmx pretyping/instantiate.cmx \ - library/lib.cmx library/libnames.cmx library/libobject.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx toplevel/recordobj.cmx \ - pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \ - library/summary.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx toplevel/discharge.cmi + kernel/indtypes.cmx kernel/inductive.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx library/library.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx toplevel/recordobj.cmx pretyping/recordops.cmx \ + kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \ + kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/discharge.cmi toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi @@ -2185,13 +2209,13 @@ toplevel/record.cmx: toplevel/class.cmx toplevel/command.cmx \ pretyping/termops.cmx interp/topconstr.cmx kernel/type_errors.cmx \ lib/util.cmx toplevel/vernacexpr.cmx toplevel/record.cmi toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \ - kernel/environ.cmi library/global.cmi pretyping/instantiate.cmi \ - library/lib.cmi library/libnames.cmi library/nameops.cmi kernel/names.cmi \ + kernel/environ.cmi library/global.cmi library/lib.cmi \ + library/libnames.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi pretyping/recordops.cmi kernel/term.cmi \ lib/util.cmi toplevel/recordobj.cmi toplevel/recordobj.cmx: pretyping/classops.cmx library/declare.cmx \ - kernel/environ.cmx library/global.cmx pretyping/instantiate.cmx \ - library/lib.cmx library/libnames.cmx library/nameops.cmx kernel/names.cmx \ + kernel/environ.cmx library/global.cmx library/lib.cmx \ + library/libnames.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx pretyping/recordops.cmx kernel/term.cmx \ lib/util.cmx toplevel/recordobj.cmi toplevel/toplevel.cmo: toplevel/cerrors.cmi library/lib.cmi \ @@ -2204,20 +2228,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.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: interp/constrextern.cmi interp/constrintern.cmi \ - parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \ - kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ - lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \ - library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ - proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \ - parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \ - kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ - lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \ - library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ - proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ @@ -2282,6 +2292,20 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi +toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \ + parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \ + kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ + lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \ + library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ + proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \ + parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \ + kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ + lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \ + library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \ interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi library/lib.cmi \ @@ -2368,6 +2392,12 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \ + contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \ + contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \ kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \ @@ -2382,12 +2412,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \ toplevel/record.cmx kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \ - contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \ - contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: interp/constrintern.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi kernel/term.cmi \ pretyping/termops.cmi contrib/correctness/pdb.cmi @@ -2799,33 +2823,31 @@ contrib/funind/tacinvutils.cmx: interp/coqlib.cmx kernel/declarations.cmx \ contrib/interface/blast.cmo: tactics/auto.cmi proofs/clenv.cmi \ toplevel/command.cmi contrib/interface/ctast.cmo kernel/declarations.cmi \ library/declare.cmi tactics/eauto.cmi kernel/environ.cmi \ - tactics/equality.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ - lib/explore.cmi library/global.cmi tactics/hipattern.cmi \ - kernel/inductive.cmi proofs/logic.cmi library/nameops.cmi \ - kernel/names.cmi pretyping/pattern.cmi contrib/interface/pbp.cmi \ - parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacentries.cmi toplevel/vernacinterp.cmi \ - contrib/interface/blast.cmi + tactics/equality.cmi pretyping/evd.cmi lib/explore.cmi library/global.cmi \ + tactics/hipattern.cmi kernel/inductive.cmi proofs/logic.cmi \ + library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi \ + contrib/interface/pbp.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ + parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi tactics/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacinterp.cmi contrib/interface/blast.cmi contrib/interface/blast.cmx: tactics/auto.cmx proofs/clenv.cmx \ toplevel/command.cmx contrib/interface/ctast.cmx kernel/declarations.cmx \ library/declare.cmx tactics/eauto.cmx kernel/environ.cmx \ - tactics/equality.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ - lib/explore.cmx library/global.cmx tactics/hipattern.cmx \ - kernel/inductive.cmx proofs/logic.cmx library/nameops.cmx \ - kernel/names.cmx pretyping/pattern.cmx contrib/interface/pbp.cmx \ - parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx proofs/refiner.cmx \ - kernel/sign.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacentries.cmx toplevel/vernacinterp.cmx \ - contrib/interface/blast.cmi + tactics/equality.cmx pretyping/evd.cmx lib/explore.cmx library/global.cmx \ + tactics/hipattern.cmx kernel/inductive.cmx proofs/logic.cmx \ + library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx \ + contrib/interface/pbp.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ + parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + proofs/refiner.cmx kernel/sign.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacinterp.cmx contrib/interface/blast.cmi contrib/interface/centaur.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/blast.cmi toplevel/cerrors.cmi pretyping/classops.cmi \ toplevel/command.cmi interp/constrintern.cmi parsing/coqast.cmi \ @@ -2964,6 +2986,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -2988,14 +3018,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \ pretyping/termops.cmx contrib/interface/translate.cmx \ pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \ @@ -3121,15 +3143,15 @@ contrib/ring/g_ring.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ contrib/ring/ring.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ lib/util.cmx toplevel/vernacinterp.cmx contrib/ring/quote.cmo: interp/coqlib.cmi kernel/environ.cmi \ - library/global.cmi pretyping/instantiate.cmi library/library.cmi \ - pretyping/matching.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi + library/global.cmi library/library.cmi pretyping/matching.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi contrib/ring/quote.cmx: interp/coqlib.cmx kernel/environ.cmx \ - library/global.cmx pretyping/instantiate.cmx library/library.cmx \ - pretyping/matching.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx + library/global.cmx library/library.cmx pretyping/matching.cmx \ + kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx contrib/ring/ring.cmo: kernel/closure.cmi interp/constrintern.cmi \ interp/coqlib.cmi tactics/equality.cmi pretyping/evd.cmi \ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ @@ -3178,58 +3200,54 @@ contrib/romega/refl_omega.cmx: contrib/romega/const_omega.cmx \ proofs/logic.cmx kernel/names.cmx contrib/romega/omega2.cmx \ lib/options.cmx lib/pp.cmx parsing/printer.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx -contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi -contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \ kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \ kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx +contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi +contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo kernel/declarations.cmi \ library/declare.cmi library/dischargedhypsmap.cmi \ contrib/xml/doubleTypeInference.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ - library/lib.cmi library/libnames.cmi library/library.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - parsing/printer.cmi pretyping/reductionops.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/univ.cmi contrib/xml/unshare.cmi \ - lib/util.cmi + kernel/inductive.cmi pretyping/inductiveops.cmi library/lib.cmi \ + library/libnames.cmi library/library.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ + pretyping/reductionops.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/univ.cmi contrib/xml/unshare.cmi lib/util.cmi contrib/xml/cic2acic.cmx: contrib/xml/acic.cmx kernel/declarations.cmx \ library/declare.cmx library/dischargedhypsmap.cmx \ contrib/xml/doubleTypeInference.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ - library/lib.cmx library/libnames.cmx library/library.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - parsing/printer.cmx pretyping/reductionops.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/univ.cmx contrib/xml/unshare.cmx \ - lib/util.cmx + kernel/inductive.cmx pretyping/inductiveops.cmx library/lib.cmx \ + library/libnames.cmx library/library.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ + pretyping/reductionops.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/univ.cmx contrib/xml/unshare.cmx lib/util.cmx contrib/xml/doubleTypeInference.cmo: contrib/xml/acic.cmo \ kernel/conv_oracle.cmi kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi kernel/inductive.cmi pretyping/instantiate.cmi \ - library/libnames.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - pretyping/retyping.cmi pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/typeops.cmi contrib/xml/unshare.cmi \ - lib/util.cmi contrib/xml/doubleTypeInference.cmi + pretyping/evd.cmi kernel/inductive.cmi library/libnames.cmi \ + kernel/names.cmi lib/pp.cmi parsing/printer.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/typeops.cmi contrib/xml/unshare.cmi lib/util.cmi \ + contrib/xml/doubleTypeInference.cmi contrib/xml/doubleTypeInference.cmx: contrib/xml/acic.cmx \ kernel/conv_oracle.cmx kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx kernel/inductive.cmx pretyping/instantiate.cmx \ - library/libnames.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - pretyping/retyping.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/typeops.cmx contrib/xml/unshare.cmx \ - lib/util.cmx contrib/xml/doubleTypeInference.cmi + pretyping/evd.cmx kernel/inductive.cmx library/libnames.cmx \ + kernel/names.cmx lib/pp.cmx parsing/printer.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/typeops.cmx contrib/xml/unshare.cmx lib/util.cmx \ + contrib/xml/doubleTypeInference.cmi contrib/xml/proof2aproof.cmo: pretyping/evarutil.cmi pretyping/evd.cmi \ - library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi lib/pp.cmi \ - proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ - contrib/xml/unshare.cmi lib/util.cmi + library/global.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_type.cmi \ + proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ + pretyping/termops.cmi contrib/xml/unshare.cmi lib/util.cmi contrib/xml/proof2aproof.cmx: pretyping/evarutil.cmx pretyping/evd.cmx \ - library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx lib/pp.cmx \ - proofs/proof_type.cmx proofs/refiner.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ - contrib/xml/unshare.cmx lib/util.cmx + library/global.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_type.cmx \ + proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ + pretyping/termops.cmx contrib/xml/unshare.cmx lib/util.cmx contrib/xml/proofTree2Xml.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \ @@ -3246,8 +3264,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/unshare.cmx lib/util.cmx contrib/xml/xml.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/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo config/coq_config.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ @@ -3276,10 +3292,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx -ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \ - ide/utils/configwin_types.cmo ide/utils/configwin.cmi -ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \ - ide/utils/configwin_types.cmx ide/utils/configwin.cmi +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \ ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \ ide/utils/uoptions.cmi @@ -3290,6 +3304,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \ ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \ ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx +ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \ + ide/utils/configwin_types.cmo ide/utils/configwin.cmi +ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \ + ide/utils/configwin_types.cmx ide/utils/configwin.cmi ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \ ide/utils/uoptions.cmi ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \ @@ -131,14 +131,15 @@ LIBRARY=\ library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo PRETYPING=\ - pretyping/termops.cmo pretyping/evd.cmo pretyping/instantiate.cmo \ + pretyping/termops.cmo pretyping/evd.cmo \ pretyping/reductionops.cmo pretyping/inductiveops.cmo \ pretyping/rawterm.cmo pretyping/pattern.cmo \ pretyping/detyping.cmo pretyping/retyping.cmo \ pretyping/cbv.cmo pretyping/tacred.cmo \ - pretyping/pretype_errors.cmo pretyping/typing.cmo \ + pretyping/pretype_errors.cmo \ pretyping/classops.cmo pretyping/recordops.cmo pretyping/indrec.cmo \ - pretyping/evarutil.cmo pretyping/evarconv.cmo \ + pretyping/evarutil.cmo pretyping/typing.cmo \ + pretyping/unification.cmo pretyping/evarconv.cmo \ pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \ pretyping/matching.cmo @@ -175,7 +176,8 @@ PROOFS=\ proofs/tacexpr.cmo proofs/proof_type.cmo \ proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ - proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo + proofs/clenv.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \ + proofs/clenvtac.cmo TACTICS=\ tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ diff --git a/bin/.cvsignore b/bin/.cvsignore index e5e3c2104..8a0fce7d0 100644 --- a/bin/.cvsignore +++ b/bin/.cvsignore @@ -10,6 +10,7 @@ coq-tex coq-extraction coq-interface parser +parser.opt coq_vo2xml coq-interface.opt coqide.byte diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index d5236a7a9..96dd51ab8 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -38,7 +38,6 @@ open Typing;; open Util;; open Vernacentries;; open Vernacinterp;; -open Evar_refiner;; let parse_com = Pcoq.parse_string Pcoq.Constr.constr;; @@ -152,8 +151,7 @@ let pp_string x = (***************************************************************************) let unify_e_resolve (c,clenv) gls = - let (wc,kONT) = startWalk gls in - let clenv' = connect_clenv wc clenv in + let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in vernac_e_resolve_constr c gls diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli index 21c29bc98..f67019439 100644 --- a/contrib/interface/blast.mli +++ b/contrib/interface/blast.mli @@ -1,5 +1,3 @@ val blast_tac : (Tacexpr.raw_tactic_expr -> 'a) -> - int list -> - Proof_type.goal Tacmach.sigma -> - Proof_type.goal list Proof_type.sigma * Proof_type.validation;; + int list -> Proof_type.tactic diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli index ded714b62..da4bbaa09 100644 --- a/contrib/interface/debug_tac.mli +++ b/contrib/interface/debug_tac.mli @@ -1,6 +1,6 @@ val report_error : Tacexpr.glob_tactic_expr -> - Proof_type.goal Proof_type.sigma option ref -> + Proof_type.goal Evd.sigma option ref -> Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;; val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;; diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli index 43ec1274d..9daba1844 100644 --- a/contrib/interface/pbp.mli +++ b/contrib/interface/pbp.mli @@ -1,4 +1,2 @@ val pbp_tac : (Tacexpr.raw_tactic_expr -> 'a) -> - Names.identifier option -> int list -> - Proof_type.goal Tacmach.sigma -> - Proof_type.goal list Proof_type.sigma * Proof_type.validation;; + Names.identifier option -> int list -> Proof_type.tactic diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 6168fdd24..5a381b57c 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -107,7 +107,6 @@ open Pp open Util open Names open Term -open Instantiate open Pattern open Matching open Tacmach diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index d820f9e59..ec5ccc8e5 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -229,7 +229,7 @@ let typeur sigma metamap = | T.Const c -> let cb = Environ.lookup_constant c env in T.body_of_type cb.Declarations.const_type - | T.Evar ev -> Instantiate.existential_type sigma ev + | T.Evar ev -> Evd.existential_type sigma ev | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind) | T.Construct cstr -> T.body_of_type (Inductive.type_of_constructor env cstr) diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index f0e3f5e35..7faf74db8 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -89,7 +89,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = "DoubleTypeInference.double_type_of: found a non-instanciated goal" | T.Evar ((n,l) as ev) -> - let ty = Unshare.unshare (Instantiate.existential_type sigma ev) in + let ty = Unshare.unshare (Evd.existential_type sigma ev) in let jty = execute env sigma ty None in let jty = assumption_of_judgment env sigma jty in let evar_context = (Evd.map sigma n).Evd.evar_hyps in diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 165a456dc..62d4ad842 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -48,7 +48,7 @@ let nf_evar sigma ~preserve = ) | _ -> T.mkApp (c', l')) | T.Evar (e,l) when Evd.in_dom sigma e & Evd.is_defined sigma e -> - aux (Instantiate.existential_value sigma (e,l)) + aux (Evd.existential_value sigma (e,l)) | T.Evar (e,l) -> T.mkEvar (e, Array.map aux l) | T.Case (ci,p,c,bl) -> T.mkCase (ci, aux p, aux c, Array.map aux bl) | T.Fix (ln,(lna,tl,bl)) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f96ba4b87..f84aa664b 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -20,7 +20,6 @@ open Inductiveops open Sign open Reduction open Environ -open Instantiate open Declare open Impargs open Libobject diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 3f9dc5c88..ceb23cc78 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -13,7 +13,6 @@ open Pp open Term open Names open Environ -open Instantiate open Univ open Evd open Closure diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 33ad61213..3ca777647 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -13,7 +13,6 @@ open Names open Term open Reductionops open Closure -open Instantiate open Environ open Typing open Classops @@ -66,7 +65,7 @@ let evar_apprec_nobeta env isevars stack c = let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in match kind_of_term t with | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n -> - aux (existential_value (evars_of isevars) ev, stack) + aux (Evd.existential_value (evars_of isevars) ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) *) @@ -77,7 +76,7 @@ let evar_apprec env isevars stack c = let (t,stack as s') = Reductionops.apprec env sigma s in match kind_of_term t with | Evar (n,_ as ev) when Evd.is_defined sigma n -> - aux (existential_value sigma ev, stack) + aux (Evd.existential_value sigma ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 97681f918..f5b8c6288 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -18,7 +18,6 @@ open Termops open Sign open Environ open Evd -open Instantiate open Reductionops open Indrec open Pretype_errors @@ -593,3 +592,34 @@ let split_tycon loc env isevars = function let valcon_of_tycon x = x let lift_tycon = option_app (lift 1) + +(*************************************) +(* Metas *) + +let meta_val_of env mv = + let rec valrec mv = + try + (match Metamap.find mv env with + | Cltyp _ -> mkMeta mv + | Clval(b,_) -> + instance (List.map (fun mv' -> (mv',valrec mv')) + (Metaset.elements b.freemetas)) b.rebus) + with Not_found -> + mkMeta mv + in + valrec mv + +let meta_instance env b = + let c_sigma = + List.map + (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas) + in + instance c_sigma b.rebus + +let nf_meta env c = meta_instance env (mk_freelisted c) + +let meta_type env mv = + let ty = + try meta_ftype env mv + with Not_found -> error ("unknown meta ?"^string_of_int mv) in + meta_instance env ty diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 29331aa5e..a08fb3f82 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -100,3 +100,8 @@ val split_tycon : val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : type_constraint -> type_constraint + +(* Metas *) +val nf_meta : meta_map -> constr -> constr +val meta_type : meta_map -> metavariable -> types +val meta_instance : meta_map -> constr freelisted -> constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d775f9fe9..be35cb947 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -12,6 +12,7 @@ open Util open Names open Term open Sign +open Environ (* The type of mappings for existential variables *) @@ -63,3 +64,142 @@ let evar_body ev = ev.evar_body let string_of_existential ev = "?" ^ string_of_int ev let existential_of_int ev = ev + +(*******************************************************************) +(* Formerly Instantiate module *) + +let is_id_inst inst = + let is_id (id,c) = match kind_of_term c with + | Var id' -> id = id' + | _ -> false + in + List.for_all is_id inst + +(* Vérifier que les instances des let-in sont compatibles ?? *) +let instantiate_sign_including_let sign args = + let rec instrec = function + | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) + | ([],[]) -> [] + | ([],_) | (_,[]) -> + anomaly "Signature and its instance do not match" + in + instrec (sign,args) + +let instantiate_evar sign c args = + let inst = instantiate_sign_including_let sign args in + if is_id_inst inst then + c + else + replace_vars inst c + +(* Existentials. *) + +let existential_type sigma (n,args) = + let info = + try map sigma n + with Not_found -> + anomaly ("Evar "^(string_of_existential n)^" was not declared") in + let hyps = info.evar_hyps in + instantiate_evar hyps info.evar_concl (Array.to_list args) + +exception NotInstantiatedEvar + +let existential_value sigma (n,args) = + let info = map sigma n in + let hyps = info.evar_hyps in + match evar_body info with + | Evar_defined c -> + instantiate_evar hyps c (Array.to_list args) + | Evar_empty -> + raise NotInstantiatedEvar + +let existential_opt_value sigma ev = + try Some (existential_value sigma ev) + with NotInstantiatedEvar -> None + +(*******************************************************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_map} + +let sig_it x = x.it +let sig_sig x = x.sigma + +(*******************************************************************) +(* Metamaps *) + +(*******************************************************************) +(* Constraints for existential variables *) +(*******************************************************************) + +type 'a freelisted = { + rebus : 'a; + freemetas : Intset.t } + +(* Collects all metavars appearing in a constr *) +let metavars_of c = + let rec collrec acc c = + match kind_of_term c with + | Meta mv -> Intset.add mv acc + | _ -> fold_constr collrec acc c + in + collrec Intset.empty c + +let mk_freelisted c = + { rebus = c; freemetas = metavars_of c } + + +(* Clausal environments *) + +type clbinding = + | Cltyp of constr freelisted + | Clval of constr freelisted * constr freelisted + +let map_fl f cfl = { cfl with rebus=f cfl.rebus } + +let map_clb f = function + | Cltyp cfl -> Cltyp (map_fl f cfl) + | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2) + +(***********************) + +module Metaset = Intset + +let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false + +module Metamap = Intmap + +let metamap_in_dom x m = + try let _ = Metamap.find x m in true with Not_found -> false + + +let metamap_to_list m = + Metamap.fold (fun n v l -> (n,v)::l) m [] + +let metamap_inv m b = + Metamap.fold (fun n v l -> if v = b then n::l else l) m [] + +type meta_map = clbinding Metamap.t + +let meta_defined env mv = + match Metamap.find mv env with + | Clval _ -> true + | Cltyp _ -> false + +let meta_fvalue env mv = + match Metamap.find mv env with + | Clval(b,_) -> b + | Cltyp _ -> anomaly "meta_fvalue: meta has no value" + +let meta_ftype env mv = + match Metamap.find mv env with + | Cltyp b -> b + | Clval(_,b) -> b + +let meta_declare mv v menv = + Metamap.add mv (Cltyp(mk_freelisted v)) menv + +let meta_assign mv v menv = + Metamap.add mv (Clval(mk_freelisted v, meta_ftype menv mv)) menv diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 567097d0d..3f9eaa5fa 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -54,3 +54,54 @@ val evar_body : evar_info -> evar_body val string_of_existential : evar -> string val existential_of_int : int -> evar + +(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has + no body and [Not_found] if it does not exist in [sigma] *) + +exception NotInstantiatedEvar +val existential_value : evar_map -> existential -> constr +val existential_type : evar_map -> existential -> types +val existential_opt_value : evar_map -> existential -> constr option + +(*************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_map} + +val sig_it : 'a sigma -> 'a +val sig_sig : 'a sigma -> evar_map + +(*************************) +(* Meta map *) + +module Metaset : Set.S with type elt = metavariable + +val meta_exists : (metavariable -> bool) -> Metaset.t -> bool + +module Metamap : Map.S with type key = metavariable + +val metamap_in_dom : metavariable -> 'a Metamap.t -> bool +val metamap_to_list : 'a Metamap.t -> (metavariable * 'a) list +val metamap_inv : 'a Metamap.t -> 'a -> metavariable list + +type 'a freelisted = { + rebus : 'a; + freemetas : Metaset.t } + +val mk_freelisted : constr -> constr freelisted +val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted + +type clbinding = + | Cltyp of constr freelisted + | Clval of constr freelisted * constr freelisted + +val map_clb : (constr -> constr) -> clbinding -> clbinding + +type meta_map = clbinding Metamap.t +val meta_defined : meta_map -> metavariable -> bool +val meta_fvalue : meta_map -> metavariable -> constr freelisted +val meta_ftype : meta_map -> metavariable -> constr freelisted +val meta_declare : metavariable -> types -> meta_map -> meta_map +val meta_assign : metavariable -> constr -> meta_map -> meta_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 8d1917d76..11cb50c83 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -19,7 +19,6 @@ open Declarations open Entries open Inductive open Inductiveops -open Instantiate open Environ open Reductionops open Typeops diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml deleted file mode 100644 index fd9ed1995..000000000 --- a/pretyping/instantiate.ml +++ /dev/null @@ -1,68 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pp -open Util -open Names -open Term -open Sign -open Evd -open Declarations -open Environ - -let is_id_inst inst = - let is_id (id,c) = match kind_of_term c with - | Var id' -> id = id' - | _ -> false - in - List.for_all is_id inst - -(* Vérifier que les instances des let-in sont compatibles ?? *) -let instantiate_sign_including_let sign args = - let rec instrec = function - | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) - | ([],[]) -> [] - | ([],_) | (_,[]) -> - anomaly "Signature and its instance do not match" - in - instrec (sign,args) - -let instantiate_evar sign c args = - let inst = instantiate_sign_including_let sign args in - if is_id_inst inst then - c - else - replace_vars inst c - -(* Existentials. *) - -let existential_type sigma (n,args) = - let info = - try Evd.map sigma n - with Not_found -> - anomaly ("Evar "^(string_of_existential n)^" was not declared") in - let hyps = info.evar_hyps in - instantiate_evar hyps info.evar_concl (Array.to_list args) - -exception NotInstantiatedEvar - -let existential_value sigma (n,args) = - let info = Evd.map sigma n in - let hyps = info.evar_hyps in - match evar_body info with - | Evar_defined c -> - instantiate_evar hyps c (Array.to_list args) - | Evar_empty -> - raise NotInstantiatedEvar - -let existential_opt_value sigma ev = - try Some (existential_value sigma ev) - with NotInstantiatedEvar -> None - diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 07d72c89e..d7407c5d1 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -26,6 +26,9 @@ type pretype_error = | OccurCheck of existential_key * constr | NotClean of existential_key * constr * hole_kind | UnsolvableImplicit of hole_kind + | CannotUnify of constr * constr + | CannotGeneralize of constr + | NoOccurrenceFound of constr (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -33,6 +36,12 @@ type pretype_error = exception PretypeError of env * pretype_error +let precatchable_exception = function + | Util.UserError _ | TypeError _ | PretypeError _ + | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + Nametab.GlobalizationError _ | PretypeError _)) -> true + | _ -> false + let nf_evar = Reductionops.nf_evar let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; @@ -141,6 +150,9 @@ let error_not_clean env sigma ev c (loc,k) = let error_unsolvable_implicit loc env sigma e = raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e)) +let error_cannot_unify env sigma (m,n) = + raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index e09a6d1d1..2f9b1dc46 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -28,6 +28,9 @@ type pretype_error = | OccurCheck of existential_key * constr | NotClean of existential_key * constr * hole_kind | UnsolvableImplicit of hole_kind + | CannotUnify of constr * constr + | CannotGeneralize of constr + | NoOccurrenceFound of constr (* Pretyping *) | VarNotFound of identifier | UnexpectedType of constr * constr @@ -35,6 +38,8 @@ type pretype_error = exception PretypeError of env * pretype_error +val precatchable_exception : exn -> bool + (* Presenting terms without solved evars *) val nf_evar : Evd.evar_map -> constr -> constr val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment @@ -82,6 +87,8 @@ val error_not_clean : val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b +val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b + (*s Ml Case errors *) val error_cant_find_case_type_loc : diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 36247edc7..dcb30c4d0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -37,7 +37,6 @@ open Dyn open Declarations open Inductive open Inductiveops -open Instantiate let lift_context n l = let k = List.length l in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c7a0dfe7a..a9fc90df2 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -17,7 +17,6 @@ open Univ open Evd open Declarations open Environ -open Instantiate open Closure open Esubst open Reduction @@ -428,7 +427,7 @@ let whd_betadeltaiota_nolet env sigma x = let rec whd_evar sigma c = match kind_of_term c with | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> - whd_evar sigma (Instantiate.existential_value sigma (ev,args)) + whd_evar sigma (Evd.existential_value sigma (ev,args)) | _ -> collapse_appl c let nf_evar sigma = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 6d2ff5d03..5a71b28d8 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -16,7 +16,6 @@ open Reductionops open Environ open Typeops open Declarations -open Instantiate let outsort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with @@ -61,7 +60,7 @@ let typeur sigma metamap = | Const c -> let cb = lookup_constant c env in body_of_type cb.const_type - | Evar ev -> existential_type sigma ev + | Evar ev -> Evd.existential_type sigma ev | Ind ind -> body_of_type (type_of_inductive env ind) | Construct cstr -> body_of_type (type_of_constructor env cstr) | Case (_,p,c,lf) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7af108a4e..9059c105f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -20,7 +20,6 @@ open Inductive open Environ open Reductionops open Closure -open Instantiate open Cbv open Rawterm @@ -94,7 +93,7 @@ let reference_opt_value sigma env = function | EvalRel n -> let (_,v,_) = lookup_rel n env in option_app (lift n) v - | EvalEvar ev -> existential_opt_value sigma ev + | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable let reference_value sigma env c = diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 7c4739b48..02e8618dc 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -89,6 +89,9 @@ let rec print_constr c = match kind_of_term c with cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++ str"}") +let term_printer = ref print_constr +let set_print_constr f = term_printer := f + (*let current_module = ref empty_dirpath let set_module m = current_module := m*) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 255e8a056..8ce7b39dc 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -20,10 +20,14 @@ open Environ val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts -(* iterators on terms *) +(* printers *) val print_sort : sorts -> std_ppcmds val print_sort_family : sorts_family -> std_ppcmds +(* debug printer: do not use to display terms to the casual user... *) val print_constr : constr -> std_ppcmds +val set_print_constr : (constr -> std_ppcmds) -> unit + +(* iterators on terms *) val prod_it : init:types -> (name * types) list -> types val lam_it : init:constr -> (name * types) list -> constr val rel_vect : int -> int -> constr array diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 844652fd8..b98ff0e7d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -21,29 +21,29 @@ open Typeops let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) -type 'a mach_flags = { - fix : bool; - nocheck : bool } - (* The typing machine without information, without universes but with existential variables. *) -let assumption_of_judgment env sigma j = +let assumption_of_judgment env (sigma,_) j = assumption_of_judgment env (j_nf_evar sigma j) -let type_judgment env sigma j = +let type_judgment env (sigma,_) j = type_judgment env (j_nf_evar sigma j) +let check_type env (sigma,_) j ty = + if not (is_conv_leq env sigma j.uj_type ty) then + error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty) -let rec execute mf env sigma cstr = +let rec execute env evd cstr = match kind_of_term cstr with | Meta n -> - error "execute: found a non-instanciated goal" + { uj_val = cstr; uj_type = Evarutil.meta_type (snd evd) n } | Evar ev -> - let ty = Instantiate.existential_type sigma ev in - let jty = execute mf env sigma ty in - let jty = assumption_of_judgment env sigma jty in + let sigma = fst evd in + let ty = Evd.existential_type sigma ev in + let jty = execute env evd ty in + let jty = assumption_of_judgment env evd jty in { uj_val = cstr; uj_type = jty } | Rel n -> @@ -62,22 +62,20 @@ let rec execute mf env sigma cstr = make_judge cstr (type_of_constructor env cstruct) | Case (ci,p,c,lf) -> - let cj = execute mf env sigma c in - let pj = execute mf env sigma p in - let lfj = execute_array mf env sigma lf in + let cj = execute env evd c in + let pj = execute env evd p in + let lfj = execute_array env evd lf in let (j,_) = judge_of_case env ci pj cj lfj in j | Fix ((vn,i as vni),recdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in + let (_,tys,_ as recdef') = execute_recdef env evd recdef in let fix = (vni,recdef') in check_fix env fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> - let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in + let (_,tys,_ as recdef') = execute_recdef env evd recdef in let cofix = (i,recdef') in check_cofix env cofix; make_judge (mkCoFix cofix) tys.(i) @@ -89,86 +87,88 @@ let rec execute mf env sigma cstr = judge_of_type u | App (f,args) -> - let j = execute mf env sigma f in - let jl = execute_array mf env sigma args in + let j = execute env evd f in + let jl = execute_array env evd args in let (j,_) = judge_of_apply env j jl in j | Lambda (name,c1,c2) -> - let j = execute mf env sigma c1 in - let var = type_judgment env sigma j in + let j = execute env evd c1 in + let var = type_judgment env evd j in let env1 = push_rel (name,None,var.utj_val) env in - let j' = execute mf env1 sigma c2 in + let j' = execute env1 evd c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> - let j = execute mf env sigma c1 in - let varj = type_judgment env sigma j in + let j = execute env evd c1 in + let varj = type_judgment env evd j in let env1 = push_rel (name,None,varj.utj_val) env in - let j' = execute mf env1 sigma c2 in - let varj' = type_judgment env1 sigma j' in + let j' = execute env1 evd c2 in + let varj' = type_judgment env1 evd j' in judge_of_product env name varj varj' | LetIn (name,c1,c2,c3) -> - let j1 = execute mf env sigma c1 in - let j2 = execute mf env sigma c2 in - let j2 = type_judgment env sigma j2 in + let j1 = execute env evd c1 in + let j2 = execute env evd c2 in + let j2 = type_judgment env evd j2 in let _ = judge_of_cast env j1 j2 in let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in - let j3 = execute mf env1 sigma c3 in + let j3 = execute env1 evd c3 in judge_of_letin env name j1 j2 j3 | Cast (c,t) -> - let cj = execute mf env sigma c in - let tj = execute mf env sigma t in - let tj = type_judgment env sigma tj in + let cj = execute env evd c in + let tj = execute env evd t in + let tj = type_judgment env evd tj in let j, _ = judge_of_cast env cj tj in j -and execute_recdef mf env sigma (names,lar,vdef) = - let larj = execute_array mf env sigma lar in - let lara = Array.map (assumption_of_judgment env sigma) larj in +and execute_recdef env evd (names,lar,vdef) = + let larj = execute_array env evd lar in + let lara = Array.map (assumption_of_judgment env evd) larj in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array mf env1 sigma vdef in + let vdefj = execute_array env1 evd vdef in let vdefv = Array.map j_val vdefj in let _ = type_fixpoint env1 names lara vdefj in (names,lara,vdefv) -and execute_array mf env sigma v = - let jl = execute_list mf env sigma (Array.to_list v) in +and execute_array env evd v = + let jl = execute_list env evd (Array.to_list v) in Array.of_list jl -and execute_list mf env sigma = function +and execute_list env evd = function | [] -> [] | c::r -> - let j = execute mf env sigma c in - let jr = execute_list mf env sigma r in + let j = execute env evd c in + let jr = execute_list env evd r in j::jr - -let safe_machine env sigma constr = - let mf = { fix = false; nocheck = false } in - execute mf env sigma constr - -let unsafe_machine env sigma constr = - let mf = { fix = false; nocheck = true } in - execute mf env sigma constr +let mcheck env evd c t = + let j = execute env evd c in + check_type env evd j t (* Type of a constr *) - -let type_of env sigma c = - let j = safe_machine env sigma c in + +let mtype_of env evd c = + let j = execute env evd c in (* No normalization: it breaks Pattern! *) (*nf_betaiota*) (body_of_type j.uj_type) -(* The typed type of a judgment. *) +let msort_of env evd c = + let j = execute env evd c in + let a = type_judgment env evd j in + a.utj_type -let execute_type env sigma constr = - let j = execute { fix=false; nocheck=true } env sigma constr in - assumption_of_judgment env sigma j +let type_of env sigma c = + mtype_of env (sigma, Evd.Metamap.empty) c +let sort_of env sigma c = + msort_of env (sigma, Evd.Metamap.empty) c +let check env sigma c = + mcheck env (sigma, Evd.Metamap.empty) c -let execute_rec_type env sigma constr = - let j = execute { fix=false; nocheck=false } env sigma constr in - assumption_of_judgment env sigma j +(* The typed type of a judgment. *) +let mtype_of_type env evd constr = + let j = execute env evd constr in + assumption_of_judgment env evd j diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8af977f10..15f3a6597 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -17,11 +17,17 @@ open Evd (* This module provides the typing machine with existential variables (but without universes). *) -val unsafe_machine : env -> evar_map -> constr -> unsafe_judgment - -val type_of : env -> evar_map -> constr -> constr - -val execute_type : env -> evar_map -> constr -> types - -val execute_rec_type : env -> evar_map -> constr -> types - +(* Typecheck a term and return its type *) +val type_of : env -> evar_map -> constr -> types +(* Typecheck a type and return its sort *) +val sort_of : env -> evar_map -> types -> sorts +(* Typecheck a term has a given type (assuming the type is OK *) +val check : env -> evar_map -> constr -> types -> unit + +(* The same but with metas... *) +val mtype_of : env -> evar_map * meta_map -> constr -> types +val msort_of : env -> evar_map * meta_map -> types -> sorts +val mcheck : env -> evar_map * meta_map -> constr -> types -> unit + +(* unused typing function... *) +val mtype_of_type : env -> evar_map * meta_map -> types -> types diff --git a/pretyping/unification.ml b/pretyping/unification.ml new file mode 100644 index 000000000..8c33a0746 --- /dev/null +++ b/pretyping/unification.ml @@ -0,0 +1,488 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Termops +open Sign +open Environ +open Evd +open Reductionops +open Rawterm +open Pattern +open Evarutil +open Pretype_errors + +(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, + gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) + +let abstract_scheme env c l lname_typ = + List.fold_left2 + (fun t (locc,a) (na,_,ta) -> + let na = match kind_of_term a with Var id -> Name id | _ -> na in + if occur_meta ta then error "cannot find a type for the generalisation" + else if occur_meta a then lambda_name env (na,ta,t) + else lambda_name env (na,ta,subst_term_occ locc a t)) + c + (List.rev l) + lname_typ + +let abstract_list_all env sigma typ c l = + let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in + let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in + try + if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + else error "abstract_list_all" + with UserError _ -> + raise (PretypeError (env,CannotGeneralize typ)) + + +(*******************************) + +type maps = evar_map * meta_map + +(* [w_Define evd sp c] + * + * Defines evar [sp] with term [c] in evar context [evd]. + * [c] is typed in the context of [sp] and evar context [evd] with + * [sp] removed to avoid circular definitions. + *) +let w_Define evd sp c = + let sigma = evars_of evd in + if Evd.is_defined sigma sp then + error "Unify.w_Define: cannot define evar twice"; + let spdecl = Evd.map sigma sp in + let env = evar_env spdecl in + let _ = + try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl + with Not_found -> + error "Instantiation contains unlegal variables" in + let spdecl' = { spdecl with evar_body = Evar_defined c } in + evars_reset_evd (Evd.add sigma sp spdecl') evd + + +(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n] + renvoie deux listes: + + metasubst:(int*constr)list récolte les instances des (Meta k) + evarsubst:(constr*constr)list récolte les instances des (Const "?k") + + Attention : pas d'unification entre les différences instances d'une + même meta ou evar, il peut rester des doublons *) + +(* Unification order: *) +(* Left to right: unifies first argument and then the other arguments *) +(*let unify_l2r x = List.rev x +(* Right to left: unifies last argument and then the other arguments *) +let unify_r2l x = x + +let sort_eqns = unify_r2l +*) + +let unify_0 env sigma cv_pb m n = + let trivial_unify pb substn m n = + if (not(occur_meta m)) & is_fconv pb env sigma m n then substn + else error_cannot_unify env sigma (m,n) in + let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n = + let cM = Evarutil.whd_castappevar sigma m + and cN = Evarutil.whd_castappevar sigma n in + match (kind_of_term cM,kind_of_term cN) with + | Meta k1, Meta k2 -> + if k1 < k2 then (k1,cN)::metasubst,evarsubst + else if k1 = k2 then substn + else (k2,cM)::metasubst,evarsubst + | Meta k, _ -> (k,cN)::metasubst,evarsubst + | _, Meta k -> (k,cM)::metasubst,evarsubst + | Evar _, _ -> metasubst,((cM,cN)::evarsubst) + | _, Evar _ -> metasubst,((cN,cM)::evarsubst) + + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 + | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN + | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) + + | App (f1,l1), App (f2,l2) -> + let len1 = Array.length l1 + and len2 = Array.length l2 in + let (f1,l1,f2,l2) = + if len1 = len2 then (f1,l1,f2,l2) + else if len1 < len2 then + let extras,restl2 = array_chop (len2-len1) l2 in + (f1, l1, appvect (f2,extras), restl2) + else + let extras,restl1 = array_chop (len1-len2) l1 in + (appvect (f1,extras), restl1, f2, l2) in + (try + array_fold_left2 (unirec_rec CONV) + (unirec_rec CONV substn f1 f2) l1 l2 + with ex when precatchable_exception ex -> + trivial_unify pb substn cM cN) + | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> + array_fold_left2 (unirec_rec CONV) + (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 + + | _ -> trivial_unify pb substn cM cN + + in + if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then + ([],[]) + else + let (mc,ec) = unirec_rec cv_pb ([],[]) m n in + ((*sort_eqns*) mc, (*sort_eqns*) ec) + + +(* Unification + * + * Procedure: + * (1) The function [unify mc wc M N] produces two lists: + * (a) a list of bindings Meta->RHS + * (b) a list of bindings EVAR->RHS + * + * The Meta->RHS bindings cannot themselves contain + * meta-vars, so they get applied eagerly to the other + * bindings. This may or may not close off all RHSs of + * the EVARs. For each EVAR whose RHS is closed off, + * we can just apply it, and go on. For each which + * is not closed off, we need to do a mimick step - + * in general, we have something like: + * + * ?X == (c e1 e2 ... ei[Meta(k)] ... en) + * + * so we need to do a mimick step, converting ?X + * into + * + * ?X -> (c ?z1 ... ?zn) + * + * of the proper types. Then, we can decompose the + * equation into + * + * ?z1 --> e1 + * ... + * ?zi --> ei[Meta(k)] + * ... + * ?zn --> en + * + * and keep on going. Whenever we find that a R.H.S. + * is closed, we can, as before, apply the constraint + * directly. Whenever we find an equation of the form: + * + * ?z -> Meta(n) + * + * we can reverse the equation, put it into our metavar + * substitution, and keep going. + * + * The most efficient mimick possible is, for each + * Meta-var remaining in the term, to declare a + * new EVAR of the same type. This is supposedly + * determinable from the clausale form context - + * we look up the metavar, take its type there, + * and apply the metavar substitution to it, to + * close it off. But this might not always work, + * since other metavars might also need to be resolved. *) + +let applyHead env sigma n c = + let evd = create_evar_defs sigma in + let rec apprec n c cty = + if n = 0 then + (evars_of evd, c) + else + match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with + | Prod (_,c1,c2) -> + let evar = + Evarutil.new_isevar evd env + (dummy_loc,Rawterm.InternalHole) c1 in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) + | _ -> error "Apply_Head_Then" + in + apprec n c (Typing.type_of env (evars_of evd) c) + +let is_mimick_head f = + match kind_of_term f with + (Const _|Var _|Rel _|Construct _|Ind _) -> true + | _ -> false + +let mimick_evar env evd hdc nargs sp = + let (sigma',c) = applyHead env (evars_of evd) nargs hdc in + evars_reset_evd sigma' evd; + w_Define evd sp c + + +(* [w_merge env sigma b metas evars] merges common instances in metas + or in evars, possibly generating new unification problems; if [b] + is true, unification of types of metas is required *) + +let w_merge env (sigma,metamap) with_types metas evars = + let evd = create_evar_defs sigma in + let mmap = ref metamap in + let ty_metas = ref [] in + let ty_evars = ref [] in + let rec w_merge_rec metas evars = + match (evars,metas) with + | ([], []) -> () + + | ((lhs,rhs)::t, metas) -> + (match kind_of_term rhs with + + | Meta k -> w_merge_rec ((k,lhs)::metas) t + + | krhs -> + (match kind_of_term lhs with + + | Evar (evn,_ as ev) -> + if is_defined_evar evd ev then + let (metas',evars') = + unify_0 env (evars_of evd) CONV rhs lhs in + w_merge_rec (metas'@metas) (evars'@t) + else begin + let rhs' = + if occur_meta rhs then subst_meta metas rhs else rhs + in + if occur_evar evn rhs' then + error "w_merge: recursive equation"; + match krhs with + | App (f,cl) when is_mimick_head f -> + (try + w_Define evd evn rhs'; + w_merge_rec metas t + with ex when precatchable_exception ex -> + mimick_evar env evd f (Array.length cl) evn; + w_merge_rec metas evars) + | _ -> + (* ensure tail recursion in non-mimickable case! *) + w_Define evd evn rhs'; + w_merge_rec metas t + end + + | _ -> anomaly "w_merge_rec")) + + | ([], (mv,n)::t) -> + if meta_defined !mmap mv then + let (metas',evars') = + unify_0 env (evars_of evd) CONV (meta_fvalue !mmap mv).rebus n in + w_merge_rec (metas'@t) evars' + else + begin + if with_types (* or occur_meta mvty *) then + (let mvty = meta_type !mmap mv in + try + let sigma = evars_of evd in + (* why not typing with the metamap ? *) + let nty = Typing.type_of env sigma (nf_meta !mmap n) in + let (mc,ec) = unify_0 env sigma CUMUL nty mvty in + ty_metas := mc @ !ty_metas; + ty_evars := ec @ !ty_evars + with e when precatchable_exception e -> ()); + mmap := meta_assign mv n !mmap; + w_merge_rec t [] + end in + (* merge constraints *) + w_merge_rec metas evars; + (if with_types then + (* merge constraints about types: if they fail, don't worry *) + try w_merge_rec !ty_metas !ty_evars +(* TODO: should backtrack *) + with e when precatchable_exception e -> ()); + (evars_of evd, !mmap) + +(* [w_unify env evd M N] + performs a unification of M and N, generating a bunch of + unification constraints in the process. These constraints + are processed, one-by-one - they may either generate new + bindings, or, if there is already a binding, new unifications, + which themselves generate new constraints. This continues + until we get failure, or we run out of constraints. + [clenv_typed_unify M N clenv] expects in addition that expected + types of metavars are unifiable with the types of their instances *) + +let w_unify_core_0 env evd with_types cv_pb m n = + let (mc,ec) = unify_0 env (fst evd) cv_pb m n in + w_merge env evd with_types mc ec + +let w_unify_0 env evd = w_unify_core_0 env evd false +let w_typed_unify env evd = w_unify_core_0 env evd true + + +(* takes a substitution s, an open term op and a closed term cl + try to find a subterm of cl which matches op, if op is just a Meta + FAIL because we cannot find a binding *) + +let iter_fail f a = + let n = Array.length a in + let rec ffail i = + if i = n then error "iter_fail" + else + try f a.(i) + with ex when precatchable_exception ex -> ffail (i+1) + in ffail 0 + +(* Tries to find an instance of term [cl] in term [op]. + Unifies [cl] to every subterm of [op] until it finds a match. + Fails if no match is found *) +let w_unify_to_subterm env (op,cl) evd = + let rec matchrec cl = + let cl = strip_outer_cast cl in + (try + if closed0 cl + then w_unify_0 env evd CONV op cl,cl + else error "Bound 1" + with ex when precatchable_exception ex -> + (match kind_of_term cl with + | App (f,args) -> + let n = Array.length args in + assert (n>0); + let c1 = mkApp (f,Array.sub args 0 (n-1)) in + let c2 = args.(n-1) in + (try + matchrec c1 + with ex when precatchable_exception ex -> + matchrec c2) + | Case(_,_,c,lf) -> (* does not search in the predicate *) + (try + matchrec c + with ex when precatchable_exception ex -> + iter_fail matchrec lf) + | LetIn(_,c1,_,c2) -> + (try + matchrec c1 + with ex when precatchable_exception ex -> + matchrec c2) + + | Fix(_,(_,types,terms)) -> + (try + iter_fail matchrec types + with ex when precatchable_exception ex -> + iter_fail matchrec terms) + + | CoFix(_,(_,types,terms)) -> + (try + iter_fail matchrec types + with ex when precatchable_exception ex -> + iter_fail matchrec terms) + + | Prod (_,t,c) -> + (try + matchrec t + with ex when precatchable_exception ex -> + matchrec c) + | Lambda (_,t,c) -> + (try + matchrec t + with ex when precatchable_exception ex -> + matchrec c) + | _ -> error "Match_subterm")) + in + try matchrec cl + with ex when precatchable_exception ex -> + raise (PretypeError (env,NoOccurrenceFound op)) + +let w_unify_to_subterm_list env allow_K oplist t evd = + List.fold_right + (fun op (evd,l) -> + if isMeta op then + if allow_K then (evd,op::l) + else error "Match_subterm" + else if occur_meta op then + let (evd',cl) = + try + (* This is up to delta for subterms w/o metas ... *) + w_unify_to_subterm env (strip_outer_cast op,t) evd + with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) + in + (evd',cl::l) + else if not allow_K & not (dependent op t) then + (* This is not up to delta ... *) + raise (PretypeError (env,NoOccurrenceFound op)) + else + (evd,op::l)) + oplist + (evd,[]) + +let secondOrderAbstraction env evd allow_K typ (p, oplist) = + let sigma = fst evd in + let (evd',cllist) = + w_unify_to_subterm_list env allow_K oplist typ evd in + let typp = meta_type (snd evd') p in + let pred = abstract_list_all env sigma typp typ cllist in + w_unify_0 env evd' CONV (mkMeta p) pred + +let w_unify2 env evd allow_K cv_pb ty1 ty2 = + let c1, oplist1 = whd_stack ty1 in + let c2, oplist2 = whd_stack ty2 in + match kind_of_term c1, kind_of_term c2 with + | Meta p1, _ -> + (* Find the predicate *) + let evd' = + secondOrderAbstraction env evd allow_K ty2 (p1,oplist1) in + (* Resume first order unification *) + w_unify_0 env evd' cv_pb (nf_meta (snd evd') ty1) ty2 + | _, Meta p2 -> + (* Find the predicate *) + let evd' = + secondOrderAbstraction env evd allow_K ty1 (p2, oplist2) in + (* Resume first order unification *) + w_unify_0 env evd' cv_pb ty1 (nf_meta (snd evd') ty2) + | _ -> error "w_unify2" + + +(* The unique unification algorithm works like this: If the pattern is + flexible, and the goal has a lambda-abstraction at the head, then + we do a first-order unification. + + If the pattern is not flexible, then we do a first-order + unification, too. + + If the pattern is flexible, and the goal doesn't have a + lambda-abstraction head, then we second-order unification. *) + +(* We decide here if first-order or second-order unif is used for Apply *) +(* We apply a term of type (ai:Ai)C and try to solve a goal C' *) +(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve *) + +(* 3-4-99 [HH] New fo/so choice heuristic : + In case we have to unify (Meta(1) args) with ([x:A]t args') + we first try second-order unification and if it fails first-order. + Before, second-order was used if the type of Meta(1) and [x:A]t was + convertible and first-order otherwise. But if failed if e.g. the type of + Meta(1) had meta-variables in it. *) +let w_unify allow_K env cv_pb ty1 ty2 evd = + let hd1,l1 = whd_stack ty1 in + let hd2,l2 = whd_stack ty2 in + match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with + (* Pattern case *) + | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) + when List.length l1 = List.length l2 -> + (try + w_typed_unify env evd cv_pb ty1 ty2 + with ex when precatchable_exception ex -> + try + w_unify2 env evd allow_K cv_pb ty1 ty2 + with PretypeError (env,NoOccurrenceFound c) as e -> raise e + | ex when precatchable_exception ex -> + error "Cannot solve a second-order unification problem") + + (* Second order case *) + | (Meta _, true, _, _ | _, _, Meta _, true) -> + (try + w_unify2 env evd allow_K cv_pb ty1 ty2 + with PretypeError (env,NoOccurrenceFound c) as e -> raise e + | ex when precatchable_exception ex -> + try + w_typed_unify env evd cv_pb ty1 ty2 + with ex when precatchable_exception ex -> + error "Cannot solve a second-order unification problem") + + (* General case: try first order *) + | _ -> w_unify_0 env evd cv_pb ty1 ty2 + diff --git a/pretyping/unification.mli b/pretyping/unification.mli new file mode 100644 index 000000000..ae276b2a8 --- /dev/null +++ b/pretyping/unification.mli @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*i*) +open Util +open Names +open Term +open Sign +open Environ +open Evd +(*i*) + +type maps = evar_map * meta_map + +val w_Define : Evarutil.evar_defs -> evar -> constr -> unit + +(* The "unique" unification fonction *) +val w_unify : + bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps + +(* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a + subterm of [t]. Constraints are added to [m] and the matched + subterm of [t] is also returned. *) +val w_unify_to_subterm : env -> constr * constr -> maps -> maps * constr + +(*i This should be in another module i*) + +(* [abstract_list_all env sigma t c l] *) +(* abstracts the terms in l over c to get a term of type t *) +(* (used in inv.ml) *) +val abstract_list_all : + env -> evar_map -> constr -> constr -> constr list -> constr diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a7e02723d..a327a09f8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -15,7 +15,6 @@ open Nameops open Term open Termops open Sign -open Instantiate open Environ open Evd open Proof_type @@ -29,29 +28,6 @@ open Rawterm open Pattern open Tacexpr -(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, - gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) - -let abstract_scheme env c l lname_typ = - List.fold_left2 - (fun t (locc,a) (na,_,ta) -> - let na = match kind_of_term a with Var id -> Name id | _ -> na in - if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) - else lambda_name env (na,ta,subst_term_occ locc a t)) - c - (List.rev l) - lname_typ - -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in - try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p - else error "abstract_list_all" - with UserError _ -> - raise (RefinerError (CannotGeneralize typ)) - (* Generator of metavariables *) let new_meta = let meta_ctr = ref 0 in @@ -72,25 +48,6 @@ let exist_to_meta sigma (emap, c) = | _ -> map_constr replace c in (!metamap, replace c) -module Metaset = Intset - -module Metamap = Intmap - -let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false - -let metamap_in_dom x m = - try let _ = Metamap.find x m in true with Not_found -> false - -let metamap_to_list m = - Metamap.fold (fun n v l -> (n,v)::l) m [] - -let metamap_inv m b = - Metamap.fold (fun n v l -> if v = b then n::l else l) m [] - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - (* collects all metavar occurences, in left-to-right order, preserving * repetitions and all. *) @@ -102,29 +59,13 @@ let collect_metas c = in List.rev (collrec [] c) -let metavars_of c = - let rec collrec acc c = - match kind_of_term c with - | Meta mv -> Metaset.add mv acc - | _ -> fold_constr collrec acc c - in - collrec Metaset.empty c - -let mk_freelisted c = - { rebus = c; freemetas = metavars_of c } - - (* Clausal environments *) -type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted - type 'a clausenv = { templval : constr freelisted; templtyp : constr freelisted; namenv : identifier Metamap.t; - env : clbinding Metamap.t; + env : meta_map; hook : 'a } type wc = named_context sigma @@ -201,12 +142,6 @@ let mk_clenv_from_n wc n (c,cty) = let mk_clenv_from wc = mk_clenv_from_n wc None -let map_fl f cfl = { cfl with rebus=f cfl.rebus } - -let map_clb f = function - | Cltyp cfl -> Cltyp (map_fl f cfl) - | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2) - let subst_clenv f sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; @@ -214,17 +149,13 @@ let subst_clenv f sub clenv = env = Metamap.map (map_clb (subst_mps sub)) clenv.env; hook = f sub clenv.hook } -let connect_clenv wc clenv = { clenv with hook = wc } +let connect_clenv gls clenv = + let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in + { clenv with hook = wc } -(* Was used in wcclausenv.ml -(* Changes the head of a clenv with (templ,templty) *) -let clenv_change_head (templ,templty) clenv = - { templval = mk_freelisted templ; - templtyp = mk_freelisted templty; - namenv = clenv.namenv; - env = clenv.env; - hook = clenv.hook } -*) +let clenv_wtactic f clenv = + let (sigma',mmap') = f (clenv.hook.sigma, clenv.env) in + {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=sigma'}} let mk_clenv_hnf_constr_type_of wc t = mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t)) @@ -294,39 +225,6 @@ let clenv_instance clenv b = let clenv_instance_term clenv c = clenv_instance clenv (mk_freelisted c) - -(* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and - * subject of Cases. - * Does check that the casted type is closed. Anyway, the refiner would - * fail in this case... *) - -let clenv_cast_meta clenv = - let rec crec u = - match kind_of_term u with - | App _ | Case _ -> crec_hd u - | Cast (c,_) when isMeta c -> u - | _ -> map_constr crec u - - and crec_hd u = - match kind_of_term (strip_outer_cast u) with - | Meta mv -> - (try - match Metamap.find mv clenv.env with - | Cltyp b -> - let b' = clenv_instance clenv b in - if occur_meta b' then u else mkCast (mkMeta mv, b') - | Clval(_) -> u - with Not_found -> - u) - | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) - | _ -> u - in - crec - - (* [clenv_pose (na,mv,cty) clenv] * returns a new clausenv which has added to it the metavar MV, * with type CTY. the name NA, if it is not ANONYMOUS, will @@ -372,13 +270,6 @@ let clenv_instance_template clenv = let clenv_instance_template_type clenv = clenv_instance clenv (clenv_template_type clenv) - -let clenv_wtactic wt clenv = - { templval = clenv.templval; - templtyp = clenv.templtyp; - namenv = clenv.namenv; - env = clenv.env; - hook = wt clenv.hook } let clenv_type_of ce c = let metamap = @@ -393,468 +284,13 @@ let clenv_type_of ce c = let clenv_instance_type_of ce c = clenv_instance ce (mk_freelisted (clenv_type_of ce c)) +let clenv_unify allow_K cv_pb t1 t2 clenv = + let env = w_env clenv.hook in + clenv_wtactic (Unification.w_unify allow_K env cv_pb t1 t2) clenv - -(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes: - - metasubst:(int*constr)list récolte les instances des (Meta k) - evarsubst:(constr*constr)list récolte les instances des (Const "?k") - - Attention : pas d'unification entre les différences instances d'une - même meta ou evar, il peut rester des doublons *) - -(* Unification order: *) -(* Left to right: unifies first argument and then the other arguments *) -(*let unify_l2r x = List.rev x -(* Right to left: unifies last argument and then the other arguments *) -let unify_r2l x = x - -let sort_eqns = unify_r2l -*) - -let unify_0 cv_pb wc m n = - let env = w_env wc - and sigma = w_Underlying wc in - let trivial_unify pb substn m n = - if (not(occur_meta m)) & is_fconv pb env sigma m n then substn - else error_cannot_unify (m,n) in - let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n = - let cM = Evarutil.whd_castappevar sigma m - and cN = Evarutil.whd_castappevar sigma n in - match (kind_of_term cM,kind_of_term cN) with - | Meta k1, Meta k2 -> - if k1 < k2 then (k1,cN)::metasubst,evarsubst - else if k1 = k2 then substn - else (k2,cM)::metasubst,evarsubst - | Meta k, _ -> (k,cN)::metasubst,evarsubst - | _, Meta k -> (k,cM)::metasubst,evarsubst - | Evar _, _ -> metasubst,((cM,cN)::evarsubst) - | _, Evar _ -> metasubst,((cN,cM)::evarsubst) - - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 - | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN - | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) - - | App (f1,l1), App (f2,l2) -> - let len1 = Array.length l1 - and len2 = Array.length l2 in - let (f1,l1,f2,l2) = - if len1 = len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) - else - let extras,restl1 = array_chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) in - (try - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn f1 f2) l1 l2 - with ex when catchable_exception ex -> - trivial_unify pb substn cM cN) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 - - | _ -> trivial_unify pb substn cM cN - - in - if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then - ([],[]) - else - let (mc,ec) = unirec_rec cv_pb ([],[]) m n in - ((*sort_eqns*) mc, (*sort_eqns*) ec) - - -(* Unification - * - * Procedure: - * (1) The function [unify mc wc M N] produces two lists: - * (a) a list of bindings Meta->RHS - * (b) a list of bindings EVAR->RHS - * - * The Meta->RHS bindings cannot themselves contain - * meta-vars, so they get applied eagerly to the other - * bindings. This may or may not close off all RHSs of - * the EVARs. For each EVAR whose RHS is closed off, - * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - - * in general, we have something like: - * - * ?X == (c e1 e2 ... ei[Meta(k)] ... en) - * - * so we need to do a mimick step, converting ?X - * into - * - * ?X -> (c ?z1 ... ?zn) - * - * of the proper types. Then, we can decompose the - * equation into - * - * ?z1 --> e1 - * ... - * ?zi --> ei[Meta(k)] - * ... - * ?zn --> en - * - * and keep on going. Whenever we find that a R.H.S. - * is closed, we can, as before, apply the constraint - * directly. Whenever we find an equation of the form: - * - * ?z -> Meta(n) - * - * we can reverse the equation, put it into our metavar - * substitution, and keep going. - * - * The most efficient mimick possible is, for each - * Meta-var remaining in the term, to declare a - * new EVAR of the same type. This is supposedly - * determinable from the clausale form context - - * we look up the metavar, take its type there, - * and apply the metavar substitution to it, to - * close it off. But this might not always work, - * since other metavars might also need to be resolved. *) - -let applyHead n c wc = - let rec apprec n c cty wc = - if n = 0 then - (wc,c) - else - match kind_of_term (w_whd_betadeltaiota wc cty) with - | Prod (_,c1,c2) -> - let evar = Evarutil.new_evar_in_sign (w_env wc) in - let (evar_n, _) = destEvar evar in - (compose - (apprec (n-1) (applist(c,[evar])) (subst1 evar c2)) - (w_Declare evar_n c1)) - wc - | _ -> error "Apply_Head_Then" - in - apprec n c (w_type_of wc c) wc - -let is_mimick_head f = - match kind_of_term f with - (Const _|Var _|Rel _|Construct _|Ind _) -> true - | _ -> false - -let rec mimick_evar hdc nargs sp wc = - let evd = Evd.map wc.sigma sp in - let wc' = extract_decl sp wc in - let (wc'', c) = applyHead nargs hdc wc' in - let (mc,ec) = unify_0 CONV wc'' (w_type_of wc'' c) (evd.evar_concl) in - let (wc''',_) = w_resrec mc ec wc'' in - if wc'== wc''' - then w_Define sp c wc - else - let wc'''' = restore_decl sp evd wc''' in - w_Define sp (Evarutil.nf_evar wc''''.sigma c) {it = wc.it ; sigma = wc''''.sigma} - -and w_Unify cv_pb m n wc = - let (mc',ec') = unify_0 cv_pb wc m n in - w_resrec mc' ec' wc - -and w_resrec metas evars wc = - match evars with - | [] -> (wc,metas) - - | (lhs,rhs) :: t -> - match kind_of_term rhs with - - | Meta k -> w_resrec ((k,lhs)::metas) t wc - - | krhs -> - match kind_of_term lhs with - - | Evar (evn,_) -> - if w_defined_evar wc evn then - let (wc',metas') = w_Unify CONV rhs lhs wc in - w_resrec (metas@metas') t wc' - else - (try - w_resrec metas t (w_Define evn rhs wc) - with ex when catchable_exception ex -> - (match krhs with - | App (f,cl) when is_mimick_head f -> - let wc' = mimick_evar f (Array.length cl) evn wc in - w_resrec metas evars wc' - | _ -> raise ex (* error "w_Unify" *))) - | _ -> anomaly "w_resrec" - - -(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en - particulier ne semblent pas vérifier que des instances différentes - d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas - provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) - -(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unifyTerms m n gls = - tclIDTAC {it = gls.it; - sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))} - -let unify m gls = - let n = pf_concl gls in unifyTerms m n gls - -(* [clenv_merge b metas evars clenv] merges common instances in metas - or in evars, possibly generating new unification problems; if [b] - is true, unification of types of metas is required *) - -let clenv_merge with_types metas evars clenv = - let ty_metas = ref [] in - let ty_evars = ref [] in - let rec clenv_resrec metas evars clenv = - match (evars,metas) with - | ([], []) -> clenv - - | ((lhs,rhs)::t, metas) -> - (match kind_of_term rhs with - - | Meta k -> clenv_resrec ((k,lhs)::metas) t clenv - - | krhs -> - (match kind_of_term lhs with - - | Evar (evn,_) -> - if w_defined_evar clenv.hook evn then - let (metas',evars') = unify_0 CONV clenv.hook rhs lhs in - clenv_resrec (metas'@metas) (evars'@t) clenv - else begin - let rhs' = - if occur_meta rhs then subst_meta metas rhs else rhs - in - if occur_evar evn rhs' then error "w_Unify"; - try - clenv_resrec metas t - (clenv_wtactic (w_Define evn rhs') clenv) - with ex when catchable_exception ex -> - (match krhs with - | App (f,cl) when is_mimick_head f -> - clenv_resrec metas evars - (clenv_wtactic - (mimick_evar f (Array.length cl) evn) - clenv) - | _ -> raise ex (* error "w_Unify" *)) - end - - | _ -> anomaly "clenv_resrec")) - - | ([], (mv,n)::t) -> - if clenv_defined clenv mv then - let (metas',evars') = - unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in - clenv_resrec (metas'@t) evars' clenv - else - begin - if with_types (* or occur_meta mvty *) then - (let mvty = clenv_instance_type clenv mv in - try - let nty = clenv_type_of clenv - (clenv_instance clenv (mk_freelisted n)) in - let (mc,ec) = unify_0 CUMUL clenv.hook nty mvty in - ty_metas := mc @ !ty_metas; - ty_evars := ec @ !ty_evars - with e when Logic.catchable_exception e -> ()); - clenv_resrec t [] (clenv_assign mv n clenv) - end in - (* merge constraints *) - let clenv' = clenv_resrec metas evars clenv in - if with_types then - (* merge constraints about types: if they fail, don't worry *) - try clenv_resrec !ty_metas !ty_evars clenv' - with e when Logic.catchable_exception e -> clenv' - else clenv' - -(* [clenv_unify M N clenv] - performs a unification of M and N, generating a bunch of - unification constraints in the process. These constraints - are processed, one-by-one - they may either generate new - bindings, or, if there is already a binding, new unifications, - which themselves generate new constraints. This continues - until we get failure, or we run out of constraints. - [clenv_typed_unify M N clenv] expects in addition that expected - types of metavars are unifiable with the types of their instances *) - -let clenv_unify_core_0 with_types cv_pb m n clenv = - let (mc,ec) = unify_0 cv_pb clenv.hook m n in - clenv_merge with_types mc ec clenv - -let clenv_unify_0 = clenv_unify_core_0 false -let clenv_typed_unify = clenv_unify_core_0 true - - -(* takes a substitution s, an open term op and a closed term cl - try to find a subterm of cl which matches op, if op is just a Meta - FAIL because we cannot find a binding *) - -let iter_fail f a = - let n = Array.length a in - let rec ffail i = - if i = n then error "iter_fail" - else - try f a.(i) - with ex when catchable_exception ex -> ffail (i+1) - in ffail 0 - -(* Tries to find an instance of term [cl] in term [op]. - Unifies [cl] to every subterm of [op] until it finds a match. - Fails if no match is found *) -let unify_to_subterm clause (op,cl) = - let rec matchrec cl = - let cl = strip_outer_cast cl in - (try - if closed0 cl - then clenv_unify_0 CONV op cl clause,cl - else error "Bound 1" - with ex when catchable_exception ex -> - (match kind_of_term cl with - | App (f,args) -> - let n = Array.length args in - assert (n>0); - let c1 = mkApp (f,Array.sub args 0 (n-1)) in - let c2 = args.(n-1) in - (try - matchrec c1 - with ex when catchable_exception ex -> - matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) - (try - matchrec c - with ex when catchable_exception ex -> - iter_fail matchrec lf) - | LetIn(_,c1,_,c2) -> - (try - matchrec c1 - with ex when catchable_exception ex -> - matchrec c2) - - | Fix(_,(_,types,terms)) -> - (try - iter_fail matchrec types - with ex when catchable_exception ex -> - iter_fail matchrec terms) - - | CoFix(_,(_,types,terms)) -> - (try - iter_fail matchrec types - with ex when catchable_exception ex -> - iter_fail matchrec terms) - - | Prod (_,t,c) -> - (try - matchrec t - with ex when catchable_exception ex -> - matchrec c) - | Lambda (_,t,c) -> - (try - matchrec t - with ex when catchable_exception ex -> - matchrec c) - | _ -> error "Match_subterm")) - in - try matchrec cl - with ex when catchable_exception ex -> - raise (RefinerError (NoOccurrenceFound op)) - -let unify_to_subterm_list allow_K clause oplist t = - List.fold_right - (fun op (clause,l) -> - if isMeta op then - if allow_K then (clause,op::l) - else error "Match_subterm" - else if occur_meta op then - let (clause',cl) = - try - (* This is up to delta for subterms w/o metas ... *) - unify_to_subterm clause (strip_outer_cast op,t) - with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op) - in - (clause',cl::l) - else if not allow_K & not (dependent op t) then - (* This is not up to delta ... *) - raise (RefinerError (NoOccurrenceFound op)) - else - (clause,op::l)) - oplist - (clause,[]) - -let secondOrderAbstraction allow_K typ (p, oplist) clause = - let env = w_env clause.hook in - let sigma = w_Underlying clause.hook in - let (clause',cllist) = unify_to_subterm_list allow_K clause oplist typ in - let typp = clenv_instance_type clause' p in - let pred = abstract_list_all env sigma typp typ cllist in - clenv_unify_0 CONV (mkMeta p) pred clause' - -let clenv_unify2 allow_K cv_pb ty1 ty2 clause = - let c1, oplist1 = whd_stack ty1 in - let c2, oplist2 = whd_stack ty2 in - match kind_of_term c1, kind_of_term c2 with - | Meta p1, _ -> - (* Find the predicate *) - let clause' = - secondOrderAbstraction allow_K ty2 (p1,oplist1) clause in - (* Resume first order unification *) - clenv_unify_0 cv_pb (clenv_instance_term clause' ty1) ty2 clause' - | _, Meta p2 -> - (* Find the predicate *) - let clause' = - secondOrderAbstraction allow_K ty1 (p2, oplist2) clause in - (* Resume first order unification *) - clenv_unify_0 cv_pb ty1 (clenv_instance_term clause' ty2) clause' - | _ -> error "clenv_unify2" - - -(* The unique unification algorithm works like this: If the pattern is - flexible, and the goal has a lambda-abstraction at the head, then - we do a first-order unification. - - If the pattern is not flexible, then we do a first-order - unification, too. - - If the pattern is flexible, and the goal doesn't have a - lambda-abstraction head, then we second-order unification. *) - -(* We decide here if first-order or second-order unif is used for Apply *) -(* We apply a term of type (ai:Ai)C and try to solve a goal C' *) -(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve *) - -(* 3-4-99 [HH] New fo/so choice heuristic : - In case we have to unify (Meta(1) args) with ([x:A]t args') - we first try second-order unification and if it fails first-order. - Before, second-order was used if the type of Meta(1) and [x:A]t was - convertible and first-order otherwise. But if failed if e.g. the type of - Meta(1) had meta-variables in it. *) -let clenv_unify allow_K cv_pb ty1 ty2 clenv = - let hd1,l1 = whd_stack ty1 in - let hd2,l2 = whd_stack ty2 in - match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with - (* Pattern case *) - | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) - when List.length l1 = List.length l2 -> - (try - clenv_typed_unify cv_pb ty1 ty2 clenv - with ex when catchable_exception ex -> - try - clenv_unify2 allow_K cv_pb ty1 ty2 clenv - with RefinerError (NoOccurrenceFound c) as e -> raise e - | ex when catchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* Second order case *) - | (Meta _, true, _, _ | _, _, Meta _, true) -> - (try - clenv_unify2 allow_K cv_pb ty1 ty2 clenv - with RefinerError (NoOccurrenceFound c) as e -> raise e - | ex when catchable_exception ex -> - try - clenv_typed_unify cv_pb ty1 ty2 clenv - with ex when catchable_exception ex -> - error "Cannot solve a second-order unification problem") - - (* General case: try first order *) - | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv - +let clenv_unique_resolver allow_K clause gl = + clenv_unify allow_K CUMUL + (clenv_instance_template_type clause) (pf_concl gl) clause (* [clenv_bchain mv clenv' clenv] * @@ -922,17 +358,6 @@ let clenv_fchain mv nextclenv clenv = let (clenv',nextclenv') = clenv_swap clenv nextclenv in clenv_bchain mv clenv' nextclenv' -let clenv_refine kONT clenv gls = - tclTHEN - (kONT clenv.hook) - (refine (clenv_instance_template clenv)) gls - -let clenv_refine_cast kONT clenv gls = - tclTHEN - (kONT clenv.hook) - (refine (clenv_cast_meta clenv (clenv_instance_template clenv))) - gls - (* [clenv_metavars clenv mv] * returns a list of the metavars which appear in the type of * the metavar mv. The list is unordered. *) @@ -960,7 +385,7 @@ let dependent_metas clenv mvs conclmetas = let clenv_dependent hyps_only clenv = let mvs = collect_metas (clenv_instance_template clenv) in - let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in + let ctyp_mvs = (mk_freelisted (clenv_instance_template_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs)) @@ -976,7 +401,7 @@ let clenv_missing c = clenv_dependent true c let clenv_independent clenv = let mvs = collect_metas (clenv_instance_template clenv) in - let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in + let ctyp_mvs = (mk_freelisted (clenv_instance_template_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs @@ -1059,7 +484,8 @@ let clenv_match_args s clause = previous case because Coercion does not handle Meta *) let c' = w_coerce clause.hook c c_typ k_typ in try clenv_unify true CONV (mkMeta k) c' clause - with RefinerError (CannotUnify (m,n)) -> + with Pretype_errors.PretypeError + (_,Pretype_errors.CannotUnify (m,n)) -> Stdpp.raise_with_loc loc (RefinerError (CannotUnifyBindingType (m,n))) in matchrec cl t @@ -1097,47 +523,8 @@ let clenv_constrain_with_bindings bl clause = matchrec clause bl -(* [clenv_pose_dependent_evars clenv] - * For each dependent evar in the clause-env which does not have a value, - * pose a value for it by constructing a fresh evar. We do this in - * left-to-right order, so that every evar's type is always closed w.r.t. - * metas. *) - -let clenv_pose_dependent_evars clenv = - let dep_mvs = clenv_dependent false clenv in - List.fold_left - (fun clenv mv -> - let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in - let (evar_n,_) = destEvar evar in - let tY = clenv_instance_type clenv mv in - let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in - clenv_assign mv evar clenv') - clenv - dep_mvs - (***************************) -let clenv_unique_resolver allow_K clause gl = - clenv_unify allow_K CUMUL - (clenv_instance_template_type clause) (pf_concl gl) clause - -let res_pf kONT clenv gls = - clenv_refine kONT (clenv_unique_resolver false clenv gls) gls - -let res_pf_cast kONT clenv gls = - clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls - -let elim_res_pf kONT clenv allow_K gls = - clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls - -let elim_res_pf_THEN_i kONT clenv tac gls = - let clenv' = (clenv_unique_resolver true clenv gls) in - tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls - -let e_res_pf kONT clenv gls = - clenv_refine kONT - (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls - (* Clausal environment for an application *) let make_clenv_binding_gen n wc (c,t) = function diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 6a0081fb4..5ca846b06 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -13,6 +13,7 @@ open Util open Names open Term open Sign +open Evd open Proof_type (*i*) @@ -26,23 +27,11 @@ val exist_to_meta : (* The Type of Constructions clausale environments. *) -module Metaset : Set.S with type elt = metavariable - -module Metamap : Map.S with type key = metavariable - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - -type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted - type 'a clausenv = { templval : constr freelisted; templtyp : constr freelisted; namenv : identifier Metamap.t; - env : clbinding Metamap.t; + env : meta_map; hook : 'a } type wc = named_context sigma (* for a better reading of the following *) @@ -67,11 +56,10 @@ val mk_clenv_type_of : wc -> constr -> wc clausenv val subst_clenv : (substitution -> 'a -> 'a) -> substitution -> 'a clausenv -> 'a clausenv +val clenv_wtactic : + (evar_map * meta_map -> evar_map * meta_map) -> wc clausenv -> wc clausenv -val connect_clenv : wc -> 'a clausenv -> wc clausenv -(*i Was used in wcclausenv.ml -val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv -i*) +val connect_clenv : goal sigma -> 'a clausenv -> wc clausenv val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv val clenv_instance_term : wc clausenv -> constr -> constr val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv @@ -80,6 +68,7 @@ val clenv_template_type : 'a clausenv -> constr freelisted val clenv_instance_type : wc clausenv -> metavariable -> constr val clenv_instance_template : wc clausenv -> constr val clenv_instance_template_type : wc clausenv -> constr +val clenv_instance : 'a clausenv -> constr freelisted -> constr val clenv_type_of : wc clausenv -> constr -> constr val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv @@ -87,9 +76,6 @@ val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv (* Unification with clenv *) type arg_bindings = (int * constr) list -val unify_0 : - Reductionops.conv_pb -> wc -> constr -> constr - -> Termops.metamap * (constr * constr) list val clenv_unify : bool -> Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv @@ -99,6 +85,7 @@ val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv (* Bindings *) val clenv_independent : wc clausenv -> metavariable list +val clenv_dependent : bool -> 'a clausenv -> metavariable list val clenv_missing : 'a clausenv -> metavariable list val clenv_constrain_missing_args : (* Used in user contrib Lannion *) constr list -> wc clausenv -> wc clausenv @@ -113,30 +100,5 @@ val make_clenv_binding_apply : val make_clenv_binding : wc -> constr * constr -> types Rawterm.bindings -> wc clausenv -(* Tactics *) -val unify : constr -> tactic -val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic -val res_pf : (wc -> tactic) -> wc clausenv -> tactic -val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic -val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic -val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic -val elim_res_pf_THEN_i : - (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic - (* Pretty-print *) val pr_clenv : 'a clausenv -> Pp.std_ppcmds - -(* Exported for debugging *) -val unify_to_subterm : - wc clausenv -> constr * constr -> wc clausenv * constr -val unify_to_subterm_list : - bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list -val clenv_typed_unify : - Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv - -(*i This should be in another module i*) - -(* [abstract_list_all env sigma t c l] *) -(* abstracts the terms in l over c to get a term of type t *) -val abstract_list_all : - Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml new file mode 100644 index 000000000..2b33d142f --- /dev/null +++ b/proofs/clenvtac.ml @@ -0,0 +1,133 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Termops +open Sign +open Environ +open Evd +open Proof_type +open Refiner +open Proof_trees +open Logic +open Reductionops +open Tacmach +open Evar_refiner +open Rawterm +open Pattern +open Tacexpr +open Clenv + + +let clenv_wtactic wt clenv = + { templval = clenv.templval; + templtyp = clenv.templtyp; + namenv = clenv.namenv; + env = clenv.env; + hook = wt clenv.hook } + +(* This function put casts around metavariables whose type could not be + * infered by the refiner, that is head of applications, predicates and + * subject of Cases. + * Does check that the casted type is closed. Anyway, the refiner would + * fail in this case... *) + +let clenv_cast_meta clenv = + let rec crec u = + match kind_of_term u with + | App _ | Case _ -> crec_hd u + | Cast (c,_) when isMeta c -> u + | _ -> map_constr crec u + + and crec_hd u = + match kind_of_term (strip_outer_cast u) with + | Meta mv -> + (try + match Metamap.find mv clenv.env with + | Cltyp b -> + let b' = clenv_instance clenv b in + if occur_meta b' then u else mkCast (mkMeta mv, b') + | Clval(_) -> u + with Not_found -> + u) + | App(f,args) -> mkApp (crec_hd f, Array.map crec args) + | Case(ci,p,c,br) -> + mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | _ -> u + in + crec + + +let clenv_refine kONT clenv gls = + tclTHEN + (kONT clenv.hook) + (refine (clenv_instance_template clenv)) gls + +let clenv_refine_cast kONT clenv gls = + tclTHEN + (kONT clenv.hook) + (refine (clenv_cast_meta clenv (clenv_instance_template clenv))) + gls + +let res_pf kONT clenv gls = + clenv_refine kONT (clenv_unique_resolver false clenv gls) gls + +let res_pf_cast kONT clenv gls = + clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls + +let elim_res_pf kONT clenv allow_K gls = + clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls + +let elim_res_pf_THEN_i kONT clenv tac gls = + let clenv' = (clenv_unique_resolver true clenv gls) in + tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls + +(* [clenv_pose_dependent_evars clenv] + * For each dependent evar in the clause-env which does not have a value, + * pose a value for it by constructing a fresh evar. We do this in + * left-to-right order, so that every evar's type is always closed w.r.t. + * metas. *) + +let clenv_pose_dependent_evars clenv = + let dep_mvs = clenv_dependent false clenv in + List.fold_left + (fun clenv mv -> + let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in + let (evar_n,_) = destEvar evar in + let tY = clenv_instance_type clenv mv in + let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in + clenv_assign mv evar clenv') + clenv + dep_mvs + +let e_res_pf kONT clenv gls = + clenv_refine kONT + (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls + + + +(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en + particulier ne semblent pas vérifier que des instances différentes + d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas + provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) + +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unifyTerms m n gls = + let env = pf_env gls in + let sigma = project gls in + tclIDTAC {it = gls.it; + sigma = fst (Unification.w_unify false env CONV m n (sigma,Evd.Metamap.empty))} + +let unify m gls = + let n = pf_concl gls in unifyTerms m n gls diff --git a/pretyping/instantiate.mli b/proofs/clenvtac.mli index 6de258296..1dd14e773 100644 --- a/pretyping/instantiate.mli +++ b/proofs/clenvtac.mli @@ -9,17 +9,21 @@ (*i $Id$ i*) (*i*) +open Util open Names open Term -open Evd open Sign -open Environ +open Evd +open Clenv +open Proof_type (*i*) -(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has -no body and [Not_found] if it does not exist in [sigma] *) - -exception NotInstantiatedEvar -val existential_value : evar_map -> existential -> constr -val existential_type : evar_map -> existential -> types -val existential_opt_value : evar_map -> existential -> constr option +(* Tactics *) +val unify : constr -> tactic +val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic +val res_pf : (wc -> tactic) -> wc clausenv -> tactic +val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic +val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic +val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic +val elim_res_pf_THEN_i : + (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index b7cdac46a..d8dfb7d59 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -19,7 +19,6 @@ open Evd open Sign open Reductionops open Typing -open Instantiate open Tacred open Proof_trees open Proof_type diff --git a/proofs/logic.ml b/proofs/logic.ml index c2cd50706..314e3c597 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -40,12 +40,9 @@ type refiner_error = | NonLinearProof of constr (* Errors raised by the tactics *) - | CannotUnify of constr * constr | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier - | NoOccurrenceFound of constr exception RefinerError of refiner_error @@ -53,13 +50,13 @@ open Pretype_errors let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ + (* unification errors *) + | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _)) + | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _))) | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true | _ -> false -let error_cannot_unify (m,n) = - raise (RefinerError (CannotUnify (m,n))) - (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false diff --git a/proofs/logic.mli b/proofs/logic.mli index 22249d9ab..34e5b9e98 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -54,17 +54,12 @@ type refiner_error = | NonLinearProof of constr (*i Errors raised by the tactics i*) - | CannotUnify of constr * constr | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier - | NoOccurrenceFound of constr exception RefinerError of refiner_error -val error_cannot_unify : constr * constr -> 'a - val catchable_exception : exn -> bool diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 18163489e..c20b01636 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -39,12 +39,6 @@ type prim_rule = | Move of bool * identifier * identifier | Rename of identifier * identifier - -(* Signature useful to define the tactic type *) -type 'a sigma = { - it : 'a ; - sigma : evar_map } - (*s Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 0684f1b95..cecda38c5 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -67,12 +67,6 @@ type prim_rule = \end{verbatim} *) -(* The type constructor ['a sigma] adds an evar map to an object of - type ['a] (see below the form of a [goal sigma] *) -type 'a sigma = { - it : 'a ; - sigma : evar_map} - (*s Proof trees. [ref] = [None] if the goal has still to be proved, and [Some (r,l)] if the rule [r] was applied to the goal diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 7d11fd8fd..248f6b40b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -17,7 +17,6 @@ open Evd open Sign open Environ open Reductionops -open Instantiate open Type_errors open Proof_trees open Proof_type diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index ceb22229c..1b1e88e82 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -14,7 +14,6 @@ open Nameops open Sign open Term open Termops -open Instantiate open Environ open Reductionops open Evd @@ -32,7 +31,7 @@ let re_sig it gc = { it = it; sigma = gc } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -91,10 +90,6 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_execute gls = - let evc = project gls in - Typing.unsafe_machine (pf_env gls) evc - let pf_reduction_of_redexp gls re c = reduction_of_redexp re (pf_env gls) (project gls) c diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f6a55e4ab..4793924d7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -25,7 +25,7 @@ open Rawterm (* Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Proof_type.sigma;; +type 'a sigma = 'a Evd.sigma;; type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; @@ -51,7 +51,6 @@ val pf_global : goal sigma -> identifier -> constr val pf_parse_const : goal sigma -> string -> constr val pf_type_of : goal sigma -> constr -> types val pf_check_type : goal sigma -> constr -> types -> unit -val pf_execute : goal sigma -> constr -> unsafe_judgment val hnf_type_of : goal sigma -> constr -> types val pf_interp_constr : goal sigma -> Topconstr.constr_expr -> constr diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 163a49193..034e36d93 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -10,6 +10,7 @@ open Environ open Pattern +open Evd open Proof_type open Names open Tacexpr diff --git a/tactics/auto.ml b/tactics/auto.ml index 22cc44766..651b976c7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -604,8 +604,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l) (* Try unification with the precompiled clause, then use registered Apply *) let unify_resolve (c,clenv) gls = - let (wc,kONT) = startWalk gls in - let clenv' = connect_clenv wc clenv in + let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in h_simplest_apply c gls diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index c65126bbb..fc9bd3aa2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -32,7 +32,7 @@ open Rawterm let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 or occur_existential t2 then - tclTHEN (unify t1) (exact_check c) gl + tclTHEN (Clenvtac.unify t1) (exact_check c) gl else exact_check c gl let assumption id = e_give_exact (mkVar id) @@ -44,7 +44,7 @@ let e_resolve_with_bindings_tac (c,lbind) gl = let (wc,kONT) = startWalk gl in let t = w_hnf_constr wc (w_type_of wc c) in let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in - e_res_pf kONT clause gl + Clenvtac.e_res_pf kONT clause gl let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls @@ -192,8 +192,7 @@ open Auto (***************************************************************************) let unify_e_resolve (c,clenv) gls = - let (wc,kONT) = startWalk gls in - let clenv' = connect_clenv wc clenv in + let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in vernac_e_resolve_constr c gls diff --git a/tactics/equality.ml b/tactics/equality.ml index a7e8c356e..bfedc8220 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -20,7 +20,6 @@ open Inductiveops open Environ open Libnames open Reductionops -open Instantiate open Typeops open Typing open Retyping @@ -585,7 +584,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Instantiate.existential_opt_value (Evarutil.evars_of isevars) + Evd.existential_opt_value (Evarutil.evars_of isevars) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) diff --git a/tactics/inv.ml b/tactics/inv.ml index fbdd790e0..e74fc05a9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -46,7 +46,7 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then - let metas = List.map (fun n -> Metamap.find n clenv.namenv) + let metas = List.map (fun n -> Evd.Metamap.find n clenv.namenv) (collect_meta_variables ccl) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ @@ -112,7 +112,7 @@ let make_inv_predicate env sigma indf realargs id status concl = | None -> let sort = get_sort_of env sigma concl in let p = make_arity env true indf sort in - abstract_list_all env sigma p concl (realargs@[mkVar id]) in + Unification.abstract_list_all env sigma p concl (realargs@[mkVar id]) in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 19c10fd72..95546142f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -290,7 +290,7 @@ let lemInv id c gls = let (wc,kONT) = startWalk gls in let clause = mk_clenv_type_of wc c in let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in - elim_res_pf kONT clause true gls + Clenvtac.elim_res_pf kONT clause true gls with | UserError (a,b) -> errorlabstrm "LemInv" diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index a5f5f742d..f092861f1 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -800,9 +800,12 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m = let relation_rewrite c1 c2 (lft2rgt,cl) gl = let but = pf_concl gl in let (hyp,c1,c2) = - let (cl',_) = Clenv.unify_to_subterm cl (c1,but) in - let c1 = Clenv.clenv_instance_term cl' c1 in - let c2 = Clenv.clenv_instance_term cl' c2 in + let cl' = + Clenv.clenv_wtactic + (fun evd -> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd)) + cl in + let c1 = Clenv.clenv_instance_term cl' c1 in + let c2 = Clenv.clenv_instance_term cl' c2 in (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2 in let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1dbfbf17f..0e10a0b5d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -22,6 +22,7 @@ open Libnames open Refiner open Tacmach open Clenv +open Clenvtac open Pattern open Matching open Evar_refiner @@ -173,8 +174,7 @@ let clause_type cls gl = (* Functions concerning matching of clausal environments *) let pf_is_matching gls pat n = - let (wc,_) = startWalk gls in - is_matching_conv (w_env wc) (w_Underlying wc) pat n + is_matching_conv (pf_env gls) (project gls) pat n let pf_matches gls pat n = matches_conv (pf_env gls) (project gls) pat n @@ -329,12 +329,12 @@ let general_elim_then_using let indclause' = clenv_constrain_with_bindings indbindings indclause in let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in let indmv = - match kind_of_term (last_arg (clenv_template elimclause).rebus) with + match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv | _ -> error "elimination" in let pmv = - let p, _ = decompose_app (clenv_template_type elimclause).rebus in + let p, _ = decompose_app elimclause.templtyp.Evd.rebus in match kind_of_term p with | Meta p -> p | _ -> @@ -351,7 +351,7 @@ let general_elim_then_using let branchsigns = compute_construtor_signatures isrec ity in let brnames = compute_induction_names (Array.length branchsigns) allnames in let after_tac ce i gl = - let (hd,largs) = decompose_app (clenv_template_type ce).rebus in + let (hd,largs) = decompose_app ce.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 655a5b53e..d5d972111 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -31,6 +31,7 @@ open Proof_type open Logic open Evar_refiner open Clenv +open Clenvtac open Refiner open Tacticals open Hipattern @@ -438,8 +439,8 @@ let bring_hyps hyps = let apply_with_bindings (c,lbind) gl = let apply = match kind_of_term c with - | Lambda _ -> res_pf_cast - | _ -> res_pf + | Lambda _ -> Clenvtac.res_pf_cast + | _ -> Clenvtac.res_pf in let (wc,kONT) = startWalk gl in (* The actual type of the theorem. It will be matched against the @@ -452,13 +453,13 @@ let apply_with_bindings (c,lbind) gl = if n<0 then error "Apply: theorem has not enough premisses."; let clause = make_clenv_binding_apply wc n (c,thm_ty) lbind in apply kONT clause gl - with (RefinerError _|UserError _|Failure _) as exn -> + with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> let red_thm = try red_product (w_env wc) (w_Underlying wc) thm_ty with (Redelimination | UserError _) -> raise exn in try_apply red_thm in try try_apply thm_ty0 - with (RefinerError _|UserError _|Failure _) -> + with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) -> (* Last chance: if the head is a variable, apply may try second order unification *) let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 11ed968a9..b1ba1f748 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -17,7 +17,6 @@ open Term open Declarations open Entries open Inductive -open Instantiate open Reduction open Cooking open Typeops diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 01f69ce05..d6f9a990c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -371,6 +371,19 @@ let explain_wrong_case_info ctx ind ci = spc () ++ pc +let explain_cannot_unify m n = + let pm = prterm m in + let pn = prterm n in + str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ + str"with" ++ brk(1,1) ++ pn + +let explain_refiner_cannot_generalize ty = + str "Cannot find a well-typed generalisation of the goal with type : " ++ + prterm ty + +let explain_no_occurrence_found c = + str "Found no subterm matching " ++ prterm c ++ str " in the current goal" + let explain_type_error ctx err = let ctx = make_all_name_different ctx in match err with @@ -427,6 +440,9 @@ let explain_pretype_error ctx err = explain_unexpected_type ctx actual expected | NotProduct c -> explain_not_product ctx c + | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotGeneralize ty -> explain_refiner_cannot_generalize ty + | NoOccurrenceFound c -> explain_no_occurrence_found c (* Refiner errors *) @@ -445,27 +461,17 @@ let explain_refiner_occur_meta_goal t = str"generated subgoal" ++ brk(1,1) ++ prterm t ++ spc () ++ str"has metavariables in it" -let explain_refiner_cannot_applt t harg = +let explain_refiner_cannot_apply t harg = str"in refiner, a term of type " ++ brk(1,1) ++ prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ prterm harg -let explain_cannot_unify m n = - let pm = prterm m in - let pn = prterm n in - str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str"with" ++ brk(1,1) ++ pn - let explain_cannot_unify_binding_type m n = let pm = prterm m in let pn = prterm n in str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn -let explain_refiner_cannot_generalize ty = - str "Cannot find a well-typed generalisation of the goal with type : " ++ - prterm ty - let explain_refiner_not_well_typed c = str"The term " ++ prterm c ++ str" is not well-typed" @@ -480,22 +486,16 @@ let explain_non_linear_proof c = str "cannot refine with term" ++ brk(1,1) ++ prterm c ++ spc () ++ str"because a metavariable has several occurrences" -let explain_no_occurrence_found c = - str "Found no subterm matching " ++ prterm c ++ str " in the current goal" - let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | OccurMeta t -> explain_refiner_occur_meta t | OccurMetaGoal t -> explain_refiner_occur_meta_goal t - | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg - | CannotUnify (m,n) -> explain_cannot_unify m n + | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n - | CannotGeneralize ty -> explain_refiner_cannot_generalize ty | NotWellTyped c -> explain_refiner_not_well_typed c | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp | NonLinearProof c -> explain_non_linear_proof c - | NoOccurrenceFound c -> explain_no_occurrence_found c (* Inductive errors *) diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index 654c1bd3f..918909c79 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -14,7 +14,6 @@ open Names open Libnames open Nameops open Term -open Instantiate open Lib open Declare open Recordops |