diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f | |
| parent | 8f5a7bbf2e5c64d6badd9e7c39da83d07b9c6f40 (diff) | |
hiding the meta_map in evar_defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
48 files changed, 674 insertions, 749 deletions
@@ -26,9 +26,9 @@ interp/symbols.cmi: lib/bignat.cmi pretyping/classops.cmi \ interp/topconstr.cmi lib/util.cmi interp/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi \ interp/topconstr.cmi lib/util.cmi -interp/topconstr.cmi: lib/bignat.cmi lib/dyn.cmi library/libnames.cmi \ - kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi \ - lib/util.cmi +interp/topconstr.cmi: lib/bignat.cmi lib/dyn.cmi pretyping/evd.cmi \ + library/libnames.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \ + kernel/term.cmi lib/util.cmi kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/conv_oracle.cmi: kernel/closure.cmi kernel/names.cmi @@ -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 @@ -155,19 +155,20 @@ pretyping/classops.cmi: library/decl_kinds.cmo kernel/environ.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/term.cmi pretyping/clenv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \ - pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi + kernel/sign.cmi kernel/term.cmi lib/util.cmi pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \ kernel/term.cmi lib/util.cmi pretyping/detyping.cmi: kernel/environ.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi -pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ +pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evd.cmi \ pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi pretyping/evarutil.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi -pretyping/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi +pretyping/evd.cmi: library/libnames.cmi kernel/names.cmi kernel/sign.cmi \ + kernel/term.cmi lib/util.cmi pretyping/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi \ kernel/term.cmi @@ -184,9 +185,9 @@ pretyping/pretype_errors.cmi: kernel/environ.cmi pretyping/evd.cmi \ pretyping/pretyping.cmi: lib/dyn.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi -pretyping/rawterm.cmi: 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: lib/dyn.cmi pretyping/evd.cmi library/libnames.cmi \ + kernel/names.cmi library/nametab.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi pretyping/recordops.cmi: pretyping/classops.cmi library/libnames.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ library/nametab.cmi kernel/term.cmi @@ -202,8 +203,8 @@ 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 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 + pretyping/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ + lib/util.cmi proofs/clenvtac.cmi: pretyping/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 \ @@ -322,11 +323,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 \ @@ -346,9 +347,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 \ @@ -478,6 +479,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 \ @@ -500,14 +509,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 @@ -524,19 +525,21 @@ ide/undo.cmo: ide/ideutils.cmi ide/undo.cmi ide/undo.cmx: ide/ideutils.cmx ide/undo.cmi interp/constrextern.cmo: lib/bignat.cmi pretyping/classops.cmi \ kernel/declarations.cmi pretyping/detyping.cmi kernel/environ.cmi \ - library/global.cmi library/impargs.cmi kernel/inductive.cmi \ - library/lib.cmi library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ - pretyping/rawterm.cmi pretyping/recordops.cmi interp/reserve.cmi \ - kernel/sign.cmi interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/evd.cmi library/global.cmi library/impargs.cmi \ + kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi \ + pretyping/recordops.cmi interp/reserve.cmi kernel/sign.cmi \ + interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \ interp/topconstr.cmi kernel/univ.cmi lib/util.cmi interp/constrextern.cmi interp/constrextern.cmx: lib/bignat.cmx pretyping/classops.cmx \ kernel/declarations.cmx pretyping/detyping.cmx kernel/environ.cmx \ - library/global.cmx library/impargs.cmx kernel/inductive.cmx \ - library/lib.cmx library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ - pretyping/rawterm.cmx pretyping/recordops.cmx interp/reserve.cmx \ - kernel/sign.cmx interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/evd.cmx library/global.cmx library/impargs.cmx \ + kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx lib/pp.cmx pretyping/rawterm.cmx \ + pretyping/recordops.cmx interp/reserve.cmx kernel/sign.cmx \ + interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/univ.cmx lib/util.cmx interp/constrextern.cmi interp/constrintern.cmo: lib/bignat.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -584,12 +587,12 @@ interp/ppextend.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \ interp/ppextend.cmi interp/ppextend.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \ interp/ppextend.cmi -interp/reserve.cmo: library/lib.cmi library/libobject.cmi library/nameops.cmi \ - kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ - library/summary.cmi lib/util.cmi interp/reserve.cmi -interp/reserve.cmx: library/lib.cmx library/libobject.cmx library/nameops.cmx \ - kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ - library/summary.cmx lib/util.cmx interp/reserve.cmi +interp/reserve.cmo: pretyping/evd.cmi library/lib.cmi library/libobject.cmi \ + library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ + pretyping/rawterm.cmi library/summary.cmi lib/util.cmi interp/reserve.cmi +interp/reserve.cmx: pretyping/evd.cmx library/lib.cmx library/libobject.cmx \ + library/nameops.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ + pretyping/rawterm.cmx library/summary.cmx lib/util.cmx interp/reserve.cmi interp/symbols.cmo: lib/bignat.cmi pretyping/classops.cmi library/global.cmi \ lib/gmap.cmi lib/gmapl.cmi library/lib.cmi library/libnames.cmi \ library/libobject.cmi kernel/names.cmi library/nametab.cmi \ @@ -610,12 +613,14 @@ interp/syntax_def.cmx: library/lib.cmx library/libnames.cmx \ library/libobject.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx library/summary.cmx interp/symbols.cmx \ interp/topconstr.cmx lib/util.cmx interp/syntax_def.cmi -interp/topconstr.cmo: lib/bignat.cmi lib/dyn.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ - pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi interp/topconstr.cmi -interp/topconstr.cmx: lib/bignat.cmx lib/dyn.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ - pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx interp/topconstr.cmi +interp/topconstr.cmo: lib/bignat.cmi lib/dyn.cmi pretyping/evd.cmi \ + library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ + interp/topconstr.cmi +interp/topconstr.cmx: lib/bignat.cmx lib/dyn.cmx pretyping/evd.cmx \ + library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ + interp/topconstr.cmi kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/esubst.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ lib/util.cmi kernel/closure.cmi @@ -660,6 +665,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 \ @@ -668,12 +679,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 \ @@ -754,10 +759,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 @@ -766,24 +771,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 \ @@ -890,6 +885,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 @@ -1224,17 +1229,17 @@ parsing/vernacextend.cmx: parsing/argextend.cmx parsing/ast.cmx \ toplevel/vernacexpr.cmx pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \ - library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi \ + pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ + pretyping/inductiveops.cmi library/nameops.cmi kernel/names.cmi \ + lib/pp.cmi pretyping/pretype_errors.cmi pretyping/rawterm.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/cases.cmi pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \ kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \ - library/global.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmx \ + pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ + pretyping/inductiveops.cmx library/nameops.cmx kernel/names.cmx \ + lib/pp.cmx pretyping/pretype_errors.cmx pretyping/rawterm.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/cases.cmi @@ -1287,43 +1292,45 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/retyping.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/coercion.cmi pretyping/detyping.cmo: kernel/declarations.cmi kernel/environ.cmi \ - library/global.cmi library/goptions.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 \ - pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ + pretyping/evd.cmi library/global.cmi library/goptions.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 pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi kernel/univ.cmi lib/util.cmi pretyping/detyping.cmi pretyping/detyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ - library/global.cmx library/goptions.cmx kernel/inductive.cmx \ - pretyping/inductiveops.cmx library/libnames.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ - pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx \ + pretyping/evd.cmx library/global.cmx library/goptions.cmx \ + kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + lib/pp.cmx pretyping/rawterm.cmx kernel/sign.cmx kernel/term.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 \ - library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ - pretyping/recordops.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi + library/libnames.cmi kernel/names.cmi pretyping/recordops.cmi \ + kernel/reduction.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 \ - library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ - pretyping/recordops.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi + library/libnames.cmx kernel/names.cmx pretyping/recordops.cmx \ + kernel/reduction.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 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/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 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/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 library/libnames.cmi kernel/names.cmi \ + kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + pretyping/evd.cmi +pretyping/evd.cmx: kernel/environ.cmx library/libnames.cmx kernel/names.cmx \ + kernel/sign.cmx kernel/term.cmx pretyping/termops.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 library/libnames.cmi \ @@ -1398,12 +1405,12 @@ pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.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 -pretyping/rawterm.cmx: lib/dyn.cmx library/libnames.cmx kernel/names.cmx \ - library/nametab.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \ - lib/util.cmx pretyping/rawterm.cmi +pretyping/rawterm.cmo: lib/dyn.cmi pretyping/evd.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 +pretyping/rawterm.cmx: lib/dyn.cmx pretyping/evd.cmx library/libnames.cmx \ + kernel/names.cmx library/nametab.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx pretyping/rawterm.cmi pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi library/library.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi library/summary.cmi \ @@ -1616,32 +1623,34 @@ scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: tactics/btermdn.cmi pretyping/clenv.cmi \ interp/constrintern.cmi kernel/declarations.cmi tactics/dhyp.cmi \ - proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ - tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \ - library/lib.cmi library/libnames.cmi library/libobject.cmi \ - library/library.cmi proofs/logic.cmi pretyping/matching.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi \ - parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \ - library/summary.cmi proofs/tacexpr.cmo 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/vernacexpr.cmo tactics/auto.cmi + kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ + library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ + kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ + library/libobject.cmi library/library.cmi proofs/logic.cmi \ + pretyping/matching.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \ + proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + proofs/refiner.cmi kernel/sign.cmi library/summary.cmi proofs/tacexpr.cmo \ + 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/vernacexpr.cmo \ + tactics/auto.cmi tactics/auto.cmx: tactics/btermdn.cmx pretyping/clenv.cmx \ interp/constrintern.cmx kernel/declarations.cmx tactics/dhyp.cmx \ - proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ - tactics/hiddentac.cmx tactics/hipattern.cmx kernel/inductive.cmx \ - library/lib.cmx library/libnames.cmx library/libobject.cmx \ - library/library.cmx proofs/logic.cmx pretyping/matching.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx \ - parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \ - library/summary.cmx proofs/tacexpr.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/vernacexpr.cmx tactics/auto.cmi + kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ + library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ + kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ + library/libobject.cmx library/library.cmx proofs/logic.cmx \ + pretyping/matching.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \ + proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + proofs/refiner.cmx kernel/sign.cmx library/summary.cmx proofs/tacexpr.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/vernacexpr.cmx \ + tactics/auto.cmi tactics/autorewrite.cmo: parsing/ast.cmi parsing/coqast.cmi \ tactics/equality.cmi tactics/hipattern.cmi library/lib.cmi \ library/libobject.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ @@ -1961,16 +1970,16 @@ tactics/tacticals.cmo: pretyping/clenv.cmi proofs/clenvtac.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 pretyping/reductionops.cmi proofs/refiner.cmi \ - kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.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: pretyping/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 pretyping/reductionops.cmx proofs/refiner.cmx \ - kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.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: pretyping/clenv.cmi proofs/clenvtac.cmi \ interp/constrintern.cmi interp/coqlib.cmi library/decl_kinds.cmo \ @@ -2055,35 +2064,33 @@ toplevel/class.cmx: pretyping/classops.cmx library/decl_kinds.cmx \ toplevel/command.cmo: toplevel/class.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ - pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ - library/impargs.cmi pretyping/indrec.cmi kernel/indtypes.cmi \ - kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi proofs/logic.cmi \ - toplevel/metasyntax.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ - pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/safe_typing.cmi library/states.cmi interp/symbols.cmi \ - interp/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \ - kernel/typeops.cmi lib/util.cmi toplevel/vernacexpr.cmo \ - toplevel/command.cmi + pretyping/evd.cmi library/global.cmi library/impargs.cmi \ + pretyping/indrec.cmi kernel/indtypes.cmi kernel/inductive.cmi \ + library/lib.cmi library/libnames.cmi library/libobject.cmi \ + library/library.cmi proofs/logic.cmi toplevel/metasyntax.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + proofs/pfedit.cmi lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/safe_typing.cmi library/states.cmi \ + interp/symbols.cmi interp/syntax_def.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + interp/topconstr.cmi kernel/typeops.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/command.cmi toplevel/command.cmx: toplevel/class.cmx interp/constrextern.cmx \ interp/constrintern.cmx library/decl_kinds.cmx kernel/declarations.cmx \ library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ - pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ - library/impargs.cmx pretyping/indrec.cmx kernel/indtypes.cmx \ - kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx proofs/logic.cmx \ - toplevel/metasyntax.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ - pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/safe_typing.cmx library/states.cmx interp/symbols.cmx \ - interp/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ - kernel/typeops.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - toplevel/command.cmi + pretyping/evd.cmx library/global.cmx library/impargs.cmx \ + pretyping/indrec.cmx kernel/indtypes.cmx kernel/inductive.cmx \ + library/lib.cmx library/libnames.cmx library/libobject.cmx \ + library/library.cmx proofs/logic.cmx toplevel/metasyntax.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + proofs/pfedit.cmx lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/safe_typing.cmx library/states.cmx \ + interp/symbols.cmx interp/syntax_def.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/command.cmi toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \ library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ lib/system.cmi toplevel/toplevel.cmi toplevel/vernac.cmi \ @@ -2232,20 +2239,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 \ @@ -2310,6 +2303,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 \ @@ -2396,6 +2403,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 \ @@ -2410,12 +2423,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 @@ -2992,6 +2999,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: pretyping/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -3016,14 +3031,6 @@ contrib/interface/showproof.cmx: pretyping/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 \ @@ -3206,12 +3213,12 @@ 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 \ @@ -3270,8 +3277,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 \ @@ -3300,10 +3305,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 @@ -3314,6 +3317,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 \ @@ -133,15 +133,15 @@ LIBRARY=\ PRETYPING=\ 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/retyping.cmo pretyping/cbv.cmo pretyping/tacred.cmo \ pretyping/pretype_errors.cmo \ - pretyping/classops.cmo pretyping/recordops.cmo pretyping/indrec.cmo \ pretyping/evarutil.cmo pretyping/typing.cmo \ - pretyping/unification.cmo pretyping/evarconv.cmo \ - pretyping/coercion.cmo pretyping/clenv.cmo pretyping/cases.cmo \ - pretyping/pretyping.cmo pretyping/matching.cmo + pretyping/unification.cmo pretyping/recordops.cmo pretyping/evarconv.cmo \ + pretyping/classops.cmo pretyping/indrec.cmo \ + pretyping/coercion.cmo pretyping/clenv.cmo \ + pretyping/rawterm.cmo pretyping/pattern.cmo \ + pretyping/detyping.cmo \ + pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo INTERP=\ parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo interp/symbols.cmo \ @@ -1302,11 +1302,11 @@ GRAMMARNEEDEDCMO=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bignat.cmo \ lib/dyn.cmo lib/options.cmo \ lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \ - kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ - kernel/sign.cmo kernel/declarations.cmo kernel/environ.cmo\ + $(KERNEL) \ library/nameops.cmo library/libnames.cmo library/summary.cmo \ library/nametab.cmo library/libobject.cmo library/lib.cmo \ library/goptions.cmo library/decl_kinds.cmo \ + library/global.cmo pretyping/termops.cmo \ pretyping/rawterm.cmo pretyping/pattern.cmo pretyping/evd.cmo \ interp/topconstr.cmo interp/genarg.cmo \ interp/ppextend.cmo parsing/coqast.cmo parsing/ast.cmo \ diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index e4b0c944b..a2b834ffb 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -127,7 +127,7 @@ let mk_open_instance id gl m t= match t with RLambda(loc,name,_,t0)-> let t1=raux (n-1) t0 in - RLambda(loc,name,RHole (dummy_loc,BinderType name),t1) + RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=Pretyping.understand evmap env (raux m rawt) in Sign.decompose_lam_n_assum m ntt diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index b15611438..d379c5569 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -384,7 +384,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty {D.synthesized = Reductionops.nf_beta (CPropRetyping.get_type_of env evar_map - (Evarutil.refresh_universes tt)) ; + (Termops.refresh_universes tt)) ; D.expected = None} in (* Debugging only: diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 62d4ad842..5c5ac5d61 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -93,7 +93,7 @@ module ProofTreeHash = let extract_open_proof sigma pf = let module PT = Proof_type in let module L = Logic in - let sigma = ref sigma in + let evd = ref (Evd.create_evar_defs sigma) in let proof_tree_to_constr = ProofTreeHash.create 503 in let proof_tree_to_flattened_proof_tree = ProofTreeHash.create 503 in let unshared_constrs = ref S.empty in @@ -134,17 +134,18 @@ let extract_open_proof sigma pf = (*CSC: the section variables in the right order must be added too *) let evar_instance = List.map (fun (n,_) -> Term.mkRel n) sorted_rels in let env = Global.env_of_context context in - let sigma',evar = - Evarutil.new_isevar_sign env !sigma goal.Evd.evar_concl evar_instance - in - sigma := sigma' ; + let evd',evar = + Evarutil.new_evar_instance context !evd goal.Evd.evar_concl + evar_instance in + evd := evd' ; evar | _ -> Util.anomaly "Bug : a case has been forgotten in proof_extractor" in let unsharedconstr = let evar_nf_constr = - nf_evar !sigma ~preserve:(function e -> S.mem e !unshared_constrs) constr + nf_evar (Evd.evars_of !evd) + ~preserve:(function e -> S.mem e !unshared_constrs) constr in Unshare.unshare ~already_unshared:(function e -> S.mem e !unshared_constrs) @@ -152,14 +153,15 @@ let extract_open_proof sigma pf = in (*CSC: debugging stuff to be removed *) if ProofTreeHash.mem proof_tree_to_constr node then - Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") (Refiner.print_proof !sigma [] node)) ; + Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") + (Refiner.print_proof (Evd.evars_of !evd) [] node)) ; ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; unshared_constrs := S.add unsharedconstr !unshared_constrs ; unsharedconstr in let unshared_pf = unshare_proof_tree pf in let pfterm = proof_extractor [] unshared_pf in - (pfterm, !sigma, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, + (pfterm, Evd.evars_of !evd, proof_tree_to_constr, proof_tree_to_flattened_proof_tree, unshared_pf) ;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 40f7d0da0..1aac94ffd 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -88,7 +88,7 @@ let pproof p = pp(print_proof Evd.empty empty_named_context p) let prevm evd = pp(pr_decls evd) -let prevd evd = prevm(Evarutil.evars_of evd) +let prevd evd = prevm(Evd.evars_of evd) let prwc wc = pp(pr_evc wc) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 372b6c4ed..77853ade8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1231,10 +1231,10 @@ let rec cases_pattern_expr_of_constr_expr = function let rec rawconstr_of_cases_pattern = function | PatVar (loc,Name id) -> RVar (loc,id) - | PatVar (loc,Anonymous) -> RHole (loc,InternalHole) + | PatVar (loc,Anonymous) -> RHole (loc,Evd.InternalHole) | PatCstr (loc,(ind,_ as c),args,_) -> let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in - let params = list_tabulate (fun _ -> RHole (loc,InternalHole)) nparams in + let params = list_tabulate (fun _ -> RHole (loc,Evd.InternalHole)) nparams in let args = params @ List.map rawconstr_of_cases_pattern args in let f = RRef (loc,ConstructRef c) in if args = [] then f else RApp (loc,f,args) @@ -1573,7 +1573,7 @@ let rec extern inctx scopes vars r = (sub_extern false scopes vars tm, (na',option_app (fun (loc,ind,nal) -> let args = List.map (function - | Anonymous -> RHole (dummy_loc,InternalHole) + | Anonymous -> RHole (dummy_loc,Evd.InternalHole) | Name id -> RVar (dummy_loc,id)) nal in let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in (extern_type scopes vars t)) x))) tml in @@ -1794,7 +1794,7 @@ let rec raw_of_pat tenv env = function anomaly "rawconstr_of_pattern: index to an anonymous variable" with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in RVar (loc,id) - | PMeta None -> RHole (loc,InternalHole) + | PMeta None -> RHole (loc,Evd.InternalHole) | PMeta (Some n) -> RPatVar (loc,(false,n)) | PApp (f,args) -> RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 03cd671af..28f0de932 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -625,7 +625,7 @@ let locate_if_isevar loc na = function (try match na with | Name id -> Reserve.find_reserved_type id | Anonymous -> raise Not_found - with Not_found -> RHole (loc, BinderType na)) + with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x let check_hidden_implicit_parameters id (_,_,_,indnames,_) = @@ -669,8 +669,8 @@ let get_implicit_name n imps = else Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i = function - | RRef (loc,r) -> (loc,ImplicitArg (r,i)) - | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) + | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i)) + | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i)) | _ -> anomaly "Only refs have implicits" let exists_implicit_name id = @@ -908,7 +908,7 @@ let internalise sigma env allow_soapp lvar c = let p' = option_app (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> - RHole (loc, QuestionMark) + RHole (loc, Evd.QuestionMark) | CPatVar (loc, n) when allow_soapp -> RPatVar (loc, n) | CPatVar (loc, (false,n)) when Options.do_translate () -> @@ -943,7 +943,7 @@ let internalise sigma env allow_soapp lvar c = (env,bl) nal | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,ts,sc), - (na,Some(intern env def),RHole(loc,BinderType na))::bl) + (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) = let idsl_pll = List.map (intern_cases_pattern scopes ([],[]) None) lhs in diff --git a/interp/reserve.ml b/interp/reserve.ml index 167f492c8..14797930d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -89,7 +89,7 @@ let anonymize_if_reserved na t = match na with if !Options.v7 & id = id_of_string "_" then t else (try if unloc t = find_reserved_type id - then RHole (dummy_loc,BinderType na) + then RHole (dummy_loc,Evd.BinderType na) else t with Not_found -> t) | Anonymous -> t diff --git a/interp/topconstr.ml b/interp/topconstr.ml index d3b72ef78..8f9360e57 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -43,7 +43,7 @@ type aconstr = | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort - | AHole of hole_kind + | AHole of Evd.hole_kind | APatVar of patvar | ACast of aconstr * aconstr @@ -192,12 +192,12 @@ let rec subst_aconstr subst raw = | APatVar _ | ASort _ -> raw - | AHole (ImplicitArg (ref,i)) -> + | AHole (Evd.ImplicitArg (ref,i)) -> let ref' = subst_global subst ref in if ref' == ref then raw else - AHole (ImplicitArg (ref',i)) - | AHole (BinderType _ | QuestionMark | CasesType | - InternalHole | TomatchTypeParameter _) -> raw + AHole (Evd.ImplicitArg (ref',i)) + | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType | + Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw | ACast (r1,r2) -> let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in diff --git a/interp/topconstr.mli b/interp/topconstr.mli index d5046b43b..53182e34b 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -39,7 +39,7 @@ type aconstr = | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort - | AHole of hole_kind + | AHole of Evd.hole_kind | APatVar of patvar | ACast of aconstr * aconstr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 463788a22..9e10c9390 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -63,13 +63,13 @@ let error_needs_inversion env x t = (* A) Typing old cases *) (* This was previously in Indrec but creates existential holes *) -let mkExistential isevars env loc = - e_new_isevar isevars env loc (new_Type ()) +let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars = + e_new_evar isevars env ~src:src (new_Type ()) let norec_branch_scheme env isevars cstr = let rec crec env = function | d::rea -> mkProd_or_LetIn d (crec (push_rel d env) rea) - | [] -> mkExistential isevars env (dummy_loc, InternalHole) in + | [] -> mkExistential env isevars in crec env (List.rev cstr.cs_args) let rec_branch_scheme env isevars (sp,j) recargs cstr = @@ -79,8 +79,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr = let d = match dest_recarg ra with | Mrec k when k=j -> - let t = mkExistential isevars env (dummy_loc, InternalHole) - in + let t = mkExistential env isevars in mkArrow t (crec (push_rel (Anonymous,None,t) env) (List.rev (lift_rel_context 1 (List.rev rea)),reca)) @@ -89,7 +88,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr = | (name,Some b,c as d)::rea, reca -> mkLetIn (name,b, c,crec (push_rel d env) (rea,reca)) - | [],[] -> mkExistential isevars env (dummy_loc, InternalHole) + | [],[] -> mkExistential env isevars | _ -> anomaly "rec_branch_scheme" in crec env (List.rev cstr.cs_args,recargs) @@ -154,7 +153,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = let j = snd ind in (* index of inductive *) let nbrec = if isrec then count_rec_arg j recargi else 0 in let nb_arg = List.length (recargs.(i)) + nbrec in - let pred = Evarutil.refresh_universes (concl_n env sigma nb_arg ft) in + let pred = refresh_universes (concl_n env sigma nb_arg ft) in if noccur_between 1 nb_arg pred then lift (-nb_arg) pred else @@ -379,7 +378,7 @@ let push_history_pattern n current cont = *) type pattern_matching_problem = { env : env; - isevars : evar_defs ref; + isevars : Evd.evar_defs ref; pred : predicate_signature option; tomatch : tomatch_stack; history : pattern_continuation; @@ -405,15 +404,15 @@ exception NotCoercible let inh_coerce_to_ind isevars env tmloc ty tyi = let (mib,mip) = Inductive.lookup_mind_specif env tyi in - let (ntys,_) = splay_prod env (evars_of !isevars) mip.mind_nf_arity in + let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in let hole_source = match tmloc with - | Some loc -> fun i -> (loc, TomatchTypeParameter (tyi,i)) - | None -> fun _ -> (dummy_loc, InternalHole) in + | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (tyi,i)) + | None -> fun _ -> (dummy_loc, Evd.InternalHole) in let (_,evarl,_) = List.fold_right (fun (na,ty) (env,evl,n) -> (push_rel (na,None,ty) env, - (e_new_isevar isevars env (hole_source n) ty)::evl,n+1)) + (e_new_evar isevars env ~src:(hole_source n) ty)::evl,n+1)) ntys (env,[],1) in let expected_typ = applist (mkInd tyi,evarl) in (* devrait être indifférent d'exiger leq ou pas puisque pour @@ -432,17 +431,17 @@ let unify_tomatch_with_patterns isevars env tmloc typ = function (let tyi = inductive_of_constructor c in try let indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in - IsInd (typ,find_rectype env (evars_of !isevars) typ) + IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) with NotCoercible -> (* 2 cases : Not the right inductive or not an inductive at all *) try - IsInd (typ,find_rectype env (evars_of !isevars) typ) + IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) (* will try to coerce later in check_and_adjust_constructor.. *) with Not_found -> NotInd (None,typ)) (* error will be detected in check_all_variables *) | None -> - try IsInd (typ,find_rectype env (evars_of !isevars) typ) + try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) with Not_found -> NotInd (None,typ) let coerce_row typing_fun isevars env cstropt tomatch = @@ -906,7 +905,7 @@ let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k let reloc_operator (k,n) = function OpRel p when p > k -> let rec unify_clauses k pv = - let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (evars_of isevars)) p) pv in + let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv' then @@ -930,7 +929,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Empiric normalization: p may depend in a irrelevant way on args of the*) (* cstr as in [c:{_:Alpha & Beta}] Cases c of (existS a b)=>(a,b) end *) let typs = - Array.map (local_strong (whd_betaevar empty_env (evars_of !isevars))) typs + Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs in let eqns = array_map2 prepare_unif_pb typs cstrs in (* First strategy: no dependencies at all *) @@ -941,7 +940,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Heuristic to avoid comparison between non-variables algebric univs*) new_Type () else - mkExistential isevars env (loc, CasesType) + mkExistential env ~src:(loc, Evd.CasesType) isevars in if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns then @@ -1128,7 +1127,7 @@ let find_predicate loc env isevars p typs cstrs current (IndType (indf,realargs)) tms = let (dep,pred) = match p with - | Some p -> abstract_predicate env (evars_of !isevars) indf current tms p + | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p | None -> infer_predicate loc env isevars typs cstrs indf in let typ = whd_beta (applist (pred, realargs)) in if dep then @@ -1368,7 +1367,7 @@ and compile_generalization pb d rest = and compile_alias pb (deppat,nondeppat,d,t) rest = let history = simplify_history pb.history in let sign, newenv, mat = - insert_aliases pb.env (evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in + insert_aliases pb.env (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in let n = List.length sign in (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) @@ -1586,13 +1585,13 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c = (n, l, env) in let n, allargs, env = List.fold_left cook (0, [], env) tomatchs in let allargs = - List.map (fun c -> lift n (nf_betadeltaiota env (evars_of !isevars) c)) allargs in + List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in let rec build_skeleton env c = (* Don't put into normal form, it has effects on the synthesis of evars *) (* let c = whd_betadeltaiota env (evars_of isevars) c in *) (* We turn all subterms possibly dependent into an evar with maximum ctxt*) if isEvar c or List.exists (eq_constr c) allargs then - mkExistential isevars env (loc, CasesType) + mkExistential env ~src:(loc, Evd.CasesType) isevars else map_constr_with_full_binders push_rel build_skeleton env c in build_skeleton env (lift n c) @@ -1700,21 +1699,21 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function | (Some pred,x) -> let loc = loc_of_rawconstr pred in let dep, n, predj = - let isevars_copy = evars_of !isevars in + let isevars_copy = Evd.evars_of !isevars in (* We first assume the predicate is non dependent *) let ndep_arity = build_expected_arity env isevars false tomatchs in try false, nb_prod ndep_arity, typing_fun (mk_tycon ndep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := evars_reset_evd isevars_copy !isevars; + isevars := Evd.evars_reset_evd isevars_copy !isevars; (* We then assume the predicate is dependent *) let dep_arity = build_expected_arity env isevars true tomatchs in try true, nb_prod dep_arity, typing_fun (mk_tycon dep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := evars_reset_evd isevars_copy !isevars; + isevars := Evd.evars_reset_evd isevars_copy !isevars; (* Otherwise we attempt to type it without constraints, possibly *) (* failing with an error message; it may also be well-typed *) (* but fails to satisfy arity constraints in case_dependent *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 5b4ed6571..450c87a1f 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -48,7 +48,6 @@ type clausenv = { namenv : identifier Metamap.t } let cl_env ce = ce.templenv -let cl_metas ce = metas_of ce.env let cl_sigma ce = evars_of ce.env let subst_clenv sub clenv = @@ -57,14 +56,14 @@ let subst_clenv sub clenv = namenv = clenv.namenv; env = reset_evd (evars_of clenv.env, - Metamap.map (map_clb (subst_mps sub)) (cl_metas clenv)) + Metamap.map (map_clb (subst_mps sub)) (metas_of clenv.env)) clenv.env; templenv = clenv.templenv } -let clenv_nf_meta clenv c = nf_meta (cl_metas clenv) c -let clenv_meta_type clenv mv = meta_type (cl_metas clenv) mv -let clenv_value clenv = meta_instance (cl_metas clenv) clenv.templval -let clenv_type clenv = meta_instance (cl_metas clenv) clenv.templtyp +let clenv_nf_meta clenv c = nf_meta clenv.env c +let clenv_meta_type clenv mv = meta_type clenv.env mv +let clenv_value clenv = meta_instance clenv.env clenv.templval +let clenv_type clenv = meta_instance clenv.env clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -75,12 +74,12 @@ let clenv_get_type_of ce c = (function | (n,Clval(_,typ)) -> (n,typ.rebus) | (n,Cltyp typ) -> (n,typ.rebus)) - (metamap_to_list (cl_metas ce)) in + (metamap_to_list (metas_of ce.env)) in Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c -let clenv_environments bound c = +let clenv_environments evd bound c = let rec clrec (ne,e,metas) n c = match n, kind_of_term c with | (Some 0, _) -> (ne, e, List.rev metas, c) @@ -109,14 +108,15 @@ let clenv_environments bound c = clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c) | (n, _) -> (ne, e, List.rev metas, c) in - clrec (Metamap.empty,Metamap.empty,[]) bound c + clrec (Metamap.empty,evd,[]) bound c let mk_clenv_from_n gls n (c,cty) = - let (namenv,env,args,concl) = clenv_environments n cty in + let evd = create_evar_defs gls.sigma in + let (namenv,env,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; namenv = namenv; - env = mk_evar_defs (gls.sigma,env); + env = env; templenv = Global.env_of_context gls.it.evar_hyps } let mk_clenv_from gls = mk_clenv_from_n gls None @@ -138,7 +138,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) let mentions clenv mv0 = let rec menrec mv1 = try - (match Metamap.find mv1 (cl_metas clenv) with + (match Metamap.find mv1 (metas_of clenv.env) with | Clval (b,_) -> Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas | Cltyp _ -> false) @@ -147,7 +147,7 @@ let mentions clenv mv0 = in menrec -let clenv_defined clenv mv = meta_defined (cl_metas clenv) mv +let clenv_defined clenv mv = meta_defined clenv.env mv (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = @@ -155,7 +155,7 @@ let clenv_assign mv rhs clenv = if meta_exists (mentions clenv mv) rhs_fls.freemetas then error "clenv__assign: circularity in unification"; try - (match Metamap.find mv (cl_metas clenv) with + (match Metamap.find mv (metas_of clenv.env) with | Clval (fls,ty) -> if not (eq_constr fls.rebus rhs) then try @@ -167,12 +167,7 @@ let clenv_assign mv rhs clenv = anomaly "clenv_assign: non dependent metavar already assigned" else clenv - | Cltyp bty -> - { clenv with - env = reset_evd - (cl_sigma clenv, - Metamap.add mv (Clval (rhs_fls,bty)) (cl_metas clenv)) - clenv.env }) + | Cltyp _ -> {clenv with env = meta_assign mv rhs_fls.rebus clenv.env}) with Not_found -> error "clenv_assign" @@ -203,12 +198,12 @@ let collect_metas c = * returns a list of the metavars which appear in the type of * the metavar mv. The list is unordered. *) -let clenv_metavars clenv mv = (meta_ftype (cl_metas clenv) mv).freemetas +let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas let dependent_metas clenv mvs conclmetas = List.fold_right (fun mv deps -> - Metaset.union deps (clenv_metavars clenv mv)) + Metaset.union deps (clenv_metavars clenv.env mv)) mvs conclmetas let clenv_dependent hyps_only clenv = @@ -240,12 +235,9 @@ 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 (cl_env clenv) in - let (evar_n,_) = destEvar evar in - let tY = clenv_meta_type clenv mv in - let clenv' = - clenv_wtactic (w_Declare (cl_env clenv) evar_n tY) clenv in - clenv_assign mv evar clenv') + let ty = clenv_meta_type clenv mv in + let (evd,evar) = new_evar clenv.env (cl_env clenv) ty in + clenv_assign mv evar {clenv with env=evd}) clenv dep_mvs @@ -286,11 +278,7 @@ let clenv_fchain mv clenv nextclenv = end else Metamap.add mv id ne) clenv.namenv (metamap_to_list nextclenv.namenv); - env = reset_evd - (cl_sigma nextclenv, - List.fold_left (fun m (n,v) -> Metamap.add n v m) - (cl_metas clenv) (metamap_to_list (cl_metas nextclenv))) - nextclenv.env; + env = meta_merge clenv.env nextclenv.env; templenv = nextclenv.templenv } in (* unify the type of the template of [nextclenv] with the type of [mv] *) @@ -474,4 +462,4 @@ let pr_clenv clenv = in (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - (prlist pr_meta_binding (metamap_to_list (cl_metas clenv)))) + (prlist pr_meta_binding (metamap_to_list (metas_of clenv.env)))) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 30bc96338..cb53feb90 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -67,8 +67,7 @@ val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv (* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *) val clenv_unify : - bool -> Reductionops.conv_pb -> constr -> constr -> - clausenv -> clausenv + bool -> conv_pb -> constr -> constr -> clausenv -> clausenv (* unifies the concl of the goal with the type of the clenv *) val clenv_unique_resolver : diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 347bc7b8e..51fea11a2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -19,6 +19,7 @@ open Recordops open Evarutil open Evarconv open Retyping +open Evd (* Typing operations dealing with coercions *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 086bf61ba..26b646bdd 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -23,6 +23,7 @@ open Nameops open Termops open Libnames open Nametab +open Evd (****************************************************************************) (* Tools for printing of Cases *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6454e0e84..2ed26c92c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -19,6 +19,7 @@ open Classops open Recordops open Evarutil open Libnames +open Evd type flex_kind_of_term = | Rigid of constr @@ -175,13 +176,13 @@ let rec evar_conv_x env isevars pbty term1 term2 = (* Maybe convertible but since reducing can erase evars which [evar_apprec]*) (* could have found, we do it only if the terms are free of evar *) if - (not (has_undefined_isevars isevars term1) & - not (has_undefined_isevars isevars term2) & + (not (has_undefined_evars isevars term1) & + not (has_undefined_evars isevars term2) & is_fconv pbty env (evars_of isevars) term1 term2) then (isevars,true) - else if ise_undefined isevars term1 then + else if is_undefined_evar isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) - else if ise_undefined isevars term2 then + else if is_undefined_evar isevars term2 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1) else let (t1,l1) = apprec_nohdbeta env isevars term1 in @@ -438,8 +439,8 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = let (isevars',ks) = List.fold_left (fun (i,ks) b -> - let dloc = (dummy_loc,Rawterm.InternalHole) in - let (i',ev) = new_isevar i env dloc (substl ks b) in + let dloc = (dummy_loc,InternalHole) in + let (i',ev) = new_evar i env ~src:dloc (substl ks b) in (i', ev :: ks)) (isevars,[]) bs in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 5deccaa8b..41b5e05fa 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -13,7 +13,7 @@ open Term open Sign open Environ open Reductionops -open Evarutil +open Evd (*i*) (* returns exception Reduction.NotConvertible if not unifiable *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index cb4efd2e1..276c455fe 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -120,7 +120,8 @@ let exist_to_meta sigma (emap, c) = (*************************************) (* Metas *) -let meta_val_of env mv = +let meta_val_of evd mv = + let env = metas_of evd in let rec valrec mv = try (match Metamap.find mv env with @@ -152,10 +153,8 @@ let meta_type env mv = (* Creating new evars *) (**********************) -let evar_env evd = Global.env_of_context evd.evar_hyps - (* Generator of existential names *) -let new_evar = +let new_untyped_evar = let evar_ctr = ref 0 in fun () -> incr evar_ctr; existential_of_int !evar_ctr @@ -165,8 +164,8 @@ let make_evar_instance env = env ~init:[] (* create an untyped existential variable *) -let new_evar_in_sign env = - let ev = new_evar () in +let new_untyped_evar_in_sign env = + let ev = new_untyped_evar () in mkEvar (ev, Array.of_list (make_evar_instance env)) (*------------------------------------* @@ -174,20 +173,66 @@ let new_evar_in_sign env = *------------------------------------*) (* All ids of sign must be distincts! *) -let new_isevar_sign env sigma typ instance = - let sign = named_context env in +let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance = + assert (List.length instance = named_context_length sign); if not (list_distinct (ids_of_named_context sign)) then - error "new_isevar_sign: two vars have the same name"; - let newev = new_evar() in - let info = { evar_concl = typ; evar_hyps = sign; - evar_body = Evar_empty } in - (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance)) + error "new_evar_instance: two vars have the same name"; + let newev = new_untyped_evar() in + (evar_declare sign newev typ ~src:src evd, + mkEvar (newev,Array.of_list instance)) + +let make_evar_instance_with_rel env = + let n = rel_context_length (rel_context env) in + let vars = + fold_named_context + (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*)) + env ~init:[] in + snd (fold_rel_context + (fun env (_,b,_) (i,l) -> + (i-1, (*if b=None then *) mkRel i :: l (*else l*))) + env ~init:(n,vars)) + +let make_subst env args = + snd (fold_named_context + (fun env (id,b,c) (args,l as g) -> + match b, args with + | (* None *) _ , a::rest -> (rest, (id,a)::l) +(* | Some _, _ -> g*) + | _ -> anomaly "Instance does not match its signature") + env ~init:(List.rev args,[])) + +(* [new_isevar] declares a new existential in an env env with type typ *) +(* Converting the env into the sign of the evar to define *) + +let push_rel_context_to_named_context env = + let sign0 = named_context env in + let (subst,_,sign) = + Sign.fold_rel_context + (fun (na,c,t) (subst,avoid,sign) -> + let na = if na = Anonymous then Name(id_of_string"_") else na in + let id = next_name_away na avoid in + ((mkVar id)::subst, + id::avoid, + add_named_decl (id,option_app (substl subst) c, + type_app (substl subst) t) + sign)) + (rel_context env) ~init:([],ids_of_named_context sign0,sign0) + in (subst, sign) + +let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ = + let subst,sign = push_rel_context_to_named_context env in + let typ' = substl subst typ in + let instance = make_evar_instance_with_rel env in + new_evar_instance sign evd typ' ~src:src instance + +(* The same using side-effect *) +let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty = + let (evd',ev) = new_evar !evd env ~src:src ty in + evd := evd'; + ev (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) -let new_Type () = mkType (new_univ ()) - -let new_Type_sort () = Type (new_univ ()) let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) (* @@ -200,40 +245,7 @@ let judge_of_new_Type () = uj_type = mkSort (Type dummy_univ) } *) -(* This refreshes universes in types; works only for inferred types (i.e. for - types of the form (x1:A1)...(xn:An)B with B a sort or an atom in - head normal form) *) -let refresh_universes t = - let modified = ref false in - let rec refresh t = match kind_of_term t with - | Sort (Type _) -> modified := true; new_Type () - | Prod (na,u,v) -> mkProd (na,u,refresh v) - | _ -> t in - let t' = refresh t in - if !modified then t' else t -(* Declaring any type to be in the sort Type shouldn't be harmful since - cumulativity now includes Prop and Set in Type. *) -let new_type_var env sigma = - let instance = make_evar_instance env in - new_isevar_sign env sigma (new_Type ()) instance - -let split_evar_to_arrow sigma (ev,args) = - let evd = Evd.map sigma ev in - let evenv = evar_env evd in - let (sigma1,dom) = new_type_var evenv sigma in - let hyps = evd.evar_hyps in - let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in - let newenv = push_named (nvar, None, dom) evenv in - let (sigma2,rng) = new_type_var newenv sigma1 in - let x = named_hd newenv dom Anonymous in - let prod = mkProd (x, dom, subst_var nvar rng) in - let sigma3 = Evd.define sigma2 ev prod in - let evdom = fst (destEvar dom), args in - let evrng = - fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in - let prod' = mkProd (x, mkEvar evdom, mkEvar evrng) in - (sigma3,prod', evdom, evrng) (* Redefines an evar with a smaller context (i.e. it may depend on less * variables) such that c becomes closed. @@ -243,11 +255,11 @@ let split_evar_to_arrow sigma (ev,args) = * What we do is that ?2 is defined by a new evar ?4 whose context will be * a prefix of ?2's env, included in ?1's env. *) -let do_restrict_hyps sigma ev args = +let do_restrict_hyps evd ev args = let args = Array.to_list args in - let evd = Evd.map sigma ev in - let env = evar_env evd in - let hyps = evd.evar_hyps in + let evi = Evd.map (evars_of !evd) ev in + let env = evar_env evi in + let hyps = evi.evar_hyps in let (_,(rsign,ncargs)) = List.fold_left (fun (sign,(rs,na)) a -> @@ -261,10 +273,11 @@ let do_restrict_hyps sigma ev args = let sign' = List.rev rsign in let env' = reset_with_named_context sign' env in let instance = make_evar_instance env' in - let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in - let nc = refresh_universes nc in (* needed only if nc is an inferred type *) - let sigma'' = Evd.define sigma' ev nc in - (sigma'', nc) + let (evd',nc) = + new_evar_instance sign' !evd evi.evar_concl + ~src:(evar_source ev !evd) instance in + evd := Evd.evar_define ev nc evd'; + nc @@ -273,45 +286,6 @@ let do_restrict_hyps sigma ev args = * operations on the evar constraints * *------------------------------------*) -type maps = evar_map * meta_map -type evar_constraint = conv_pb * constr * constr -type evar_defs = - { evars : Evd.evar_map; - conv_pbs : evar_constraint list; - history : (existential_key * (loc * Rawterm.hole_kind)) list; - metas : Evd.meta_map } - -let mk_evar_defs (sigma,mmap) = - { evars=sigma; conv_pbs=[]; history=[]; metas=mmap } -let create_evar_defs sigma = - mk_evar_defs (sigma,Metamap.empty) -let evars_of d = d.evars -let metas_of d = d.metas -let evars_reset_evd evd d = {d with evars = evd} -let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} -let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} -let evar_source ev d = - try List.assoc ev d.history - with Failure _ -> (dummy_loc, Rawterm.InternalHole) - -(* say if the section path sp corresponds to an existential *) -let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp - -(* map the given section path to the enamed_declaration *) -let ise_map isevars sp = Evd.map isevars.evars sp - -(* define the existential of section path sp as the constr body *) -let ise_define isevars sp body = - let body = refresh_universes body in (* needed only if an inferred type *) - {isevars with evars = Evd.define isevars.evars sp body} - -let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n - -(* Does k corresponds to an (un)defined existential ? *) -let ise_undefined isevars c = match kind_of_term c with - | Evar ev -> not (is_defined_evar isevars ev) - | _ -> false - let need_restriction isevars args = not (array_for_all closed0 args) (* The list of non-instantiated existential declarations *) @@ -343,17 +317,9 @@ let real_clean env isevars ev args rhs = | Evar (ev,args) -> let args' = Array.map (subs k) args in if need_restriction !evd args' then - if Evd.is_defined !evd.evars ev then - subs k (existential_value !evd.evars (ev,args')) - else begin - let (sigma,rc) = do_restrict_hyps !evd.evars ev args' in - evd := - {!evd with - evars = sigma; - history = - (fst (destEvar rc),evar_source ev !evd):: !evd.history}; - rc - end + if Evd.is_defined_evar !evd (ev,args) then + subs k (existential_value (evars_of !evd) (ev,args')) + else do_restrict_hyps evd ev args' else mkEvar (ev,args') | Var _ -> (try List.assoc t subst with Not_found -> t) @@ -361,63 +327,9 @@ let real_clean env isevars ev args rhs = in let body = subs 0 rhs in if not (closed0 body) - then error_not_clean env !evd.evars ev body (evar_source ev !evd); + then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); (!evd,body) -let make_evar_instance_with_rel env = - let n = rel_context_length (rel_context env) in - let vars = - fold_named_context - (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*)) - env ~init:[] in - snd (fold_rel_context - (fun env (_,b,_) (i,l) -> - (i-1, (*if b=None then *) mkRel i :: l (*else l*))) - env ~init:(n,vars)) - -let make_subst env args = - snd (fold_named_context - (fun env (id,b,c) (args,l as g) -> - match b, args with - | (* None *) _ , a::rest -> (rest, (id,a)::l) -(* | Some _, _ -> g*) - | _ -> anomaly "Instance does not match its signature") - env ~init:(List.rev args,[])) - -(* [new_isevar] declares a new existential in an env env with type typ *) -(* Converting the env into the sign of the evar to define *) - -let push_rel_context_to_named_context env = - let sign0 = named_context env in - let (subst,_,sign) = - Sign.fold_rel_context - (fun (na,c,t) (subst,avoid,sign) -> - let na = if na = Anonymous then Name(id_of_string"_") else na in - let id = next_name_away na avoid in - ((mkVar id)::subst, - id::avoid, - add_named_decl (id,option_app (substl subst) c, - type_app (substl subst) t) - sign)) - (rel_context env) ~init:([],ids_of_named_context sign0,sign0) - in (subst, reset_with_named_context sign env) - -let new_isevar isevars env src typ = - let subst,env' = push_rel_context_to_named_context env in - let typ' = substl subst typ in - let instance = make_evar_instance_with_rel env in - let (sigma',evar) = new_isevar_sign env' isevars.evars typ' instance in - {isevars with - evars = sigma'; - history = (fst (destEvar evar),src)::isevars.history}, - evar - -(* The same using side-effect *) -let e_new_isevar isevars env loc ty = - let (evd',ev) = new_isevar !isevars env loc ty in - isevars := evd'; - ev - (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args) * ?sp [ sp.hyps \ args ] unifies to rhs @@ -440,24 +352,24 @@ let evar_define env isevars (ev,argsv) rhs = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in - let evi = ise_map isevars ev in + let evi = Evd.map (evars_of isevars) ev in (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev worklist rhs in - let isevars'' = ise_define isevars' ev body in + let isevars'' = Evd.evar_define ev body isevars' in isevars'',[ev] (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_undefined_isevars isevars t = - try let _ = local_strong (whd_ise isevars.evars) t in false +let has_undefined_evars isevars t = + try let _ = local_strong (whd_ise (evars_of isevars)) t in false with Uninstantiated_evar _ -> true let head_is_evar isevars = let rec hrec k = match kind_of_term k with - | Evar (n,_) -> not (Evd.is_defined isevars.evars n) + | Evar n -> not (Evd.is_defined_evar isevars n) | App (f,_) -> hrec f | Cast (c,_) -> hrec c | _ -> false @@ -515,20 +427,6 @@ let status_changed lev (pbty,t1,t2) = with Failure _ -> try List.mem (head_evar t2) lev with Failure _ -> false -let get_changed_pb isevars lev = - let (pbs,pbs1) = - List.fold_left - (fun (pbs,pbs1) pb -> - if status_changed lev pb then - (pb::pbs,pbs1) - else - (pbs,pb::pbs1)) - ([],[]) - isevars.conv_pbs - in - {isevars with conv_pbs = pbs1}, - pbs - (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint * definitions. We try to unify the xi with the yi pairwise. The pairs * that don't unify are discarded (i.e. ?i is redefined so that it does not @@ -536,7 +434,7 @@ let get_changed_pb isevars lev = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then (isevars,[]) else - let evd = Evd.map isevars.evars ev in + let evd = Evd.map (evars_of isevars) ev in let hyps = evd.evar_hyps in let (isevars',_,rsign) = array_fold_left2 @@ -549,15 +447,11 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = (isevars,hyps,[]) argsv1 argsv2 in let nsign = List.rev rsign in - let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in - let newev = new_evar () in - let info = { evar_concl = evd.evar_concl; evar_hyps = nsign; - evar_body = Evar_empty } in - {isevars with - evars = - Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs)); - history = (newev,evar_source ev isevars)::isevars.history}, - [ev] + let (evd',newev) = + new_evar isevars (reset_with_named_context nsign env) + ~src:(evar_source ev isevars) evd.evar_concl in + let evd'' = Evd.evar_define ev newev evd' in + evd'', [ev] (* Tries to solve problem t1 = t2. @@ -567,7 +461,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = - let t2 = nf_evar isevars.evars t2 in + let t2 = nf_evar (evars_of isevars) t2 in let (isevars,lsp) = match kind_of_term t2 with | Evar (n2,args2 as ev2) -> if n1 = n2 then @@ -579,7 +473,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = evar_define env isevars ev1 t2 | _ -> evar_define env isevars ev1 t2 in - let (isevars,pbs) = get_changed_pb isevars lsp in + let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left (fun (isevars,b as p) (pbty,t1,t2) -> if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) @@ -618,23 +512,29 @@ let mk_valcon c = Some c (* Refining an evar to a product or a sort *) -let refine_evar_as_arrow isevars ev = - let (sigma,prod,evdom,evrng) = split_evar_to_arrow isevars.evars ev in - let hst = evar_source (fst ev) isevars in - let isevars' = - {isevars with - evars=sigma; - history = (fst evrng,hst)::(fst evdom, hst)::isevars.history } in - (isevars',prod,evdom,evrng) - -let define_evar_as_arrow isevars ev = - let (isevars',prod,_,_) = refine_evar_as_arrow isevars ev in - isevars',prod +(* Declaring any type to be in the sort Type shouldn't be harmful since + cumulativity now includes Prop and Set in Type... + It is, but that's not too bad *) +let define_evar_as_arrow evd (ev,args) = + let evi = Evd.map (evars_of evd) ev in + let evenv = evar_env evi in + let (evd1,dom) = new_evar evd evenv (new_Type()) in + let nvar = + next_ident_away (id_of_string "x") (ids_of_named_context evi.evar_hyps) in + let newenv = push_named (nvar, None, dom) evenv in + let (evd2,rng) = + new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) in + let prod = mkProd (Name nvar, dom, subst_var nvar rng) in + let evd3 = Evd.evar_define ev prod evd2 in + let evdom = fst (destEvar dom), args in + let evrng = + fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in + let prod' = mkProd (Name nvar, mkEvar evdom, mkEvar evrng) in + (evd3,prod') let define_evar_as_sort isevars (ev,args) = let s = new_Type () in - let sigma' = Evd.define isevars.evars ev s in - evars_reset_evd sigma' isevars, destSort s + Evd.evar_define ev s isevars, destSort s (* Propagation of constraints through application and abstraction: @@ -649,9 +549,10 @@ let split_tycon loc env isevars = function let t = whd_betadeltaiota env sigma c in match kind_of_term t with | Prod (na,dom,rng) -> isevars, (na, Some dom, Some rng) - | Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) -> - let (isevars',_,evdom,evrng) = refine_evar_as_arrow isevars ev in - isevars',(Anonymous, Some (mkEvar evdom), Some (mkEvar evrng)) + | Evar ev when not (Evd.is_defined_evar isevars ev) -> + let (isevars',prod) = define_evar_as_arrow isevars ev in + let (_,dom,rng) = destProd prod in + isevars',(Anonymous, Some dom, Some rng) | _ -> error_not_product_loc loc env sigma c let valcon_of_tycon x = x diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 6d264b718..711e10707 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -46,53 +46,43 @@ val whd_castappevar : evar_map -> constr -> constr (* [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable val mk_new_meta : unit -> constr -val nf_meta : meta_map -> constr -> constr -val meta_type : meta_map -> metavariable -> types -val meta_instance : meta_map -> constr freelisted -> constr +val nf_meta : evar_defs -> constr -> constr +val meta_type : evar_defs -> metavariable -> types +val meta_instance : evar_defs -> constr freelisted -> constr (* [exist_to_meta] generates new metavariables for each existential and performs the replacement in the given constr *) val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr) -(* Creating new existential variables *) -val new_evar : unit -> evar -val new_evar_in_sign : env -> constr - -val evar_env : evar_info -> env (***********************************************************) -type maps = evar_map * meta_map -type evar_defs -val evars_of : evar_defs -> evar_map -val metas_of : evar_defs -> meta_map - -val non_instantiated : evar_map -> (evar * evar_info) list - -val mk_evar_defs : maps -> evar_defs -(* the same with empty meta map: *) -val create_evar_defs : evar_map -> evar_defs -val evars_reset_evd : evar_map -> evar_defs -> evar_defs -val reset_evd : maps -> evar_defs -> evar_defs -val evar_source : existential_key -> evar_defs -> loc * hole_kind - -type evar_constraint = conv_pb * constr * constr -val add_conv_pb : evar_constraint -> evar_defs -> evar_defs - -val is_defined_evar : evar_defs -> existential -> bool -val ise_undefined : evar_defs -> constr -> bool -val has_undefined_isevars : evar_defs -> constr -> bool - -val new_isevar_sign : - Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list -> - Evd.evar_map * Term.constr +(* Creating a fresh evar given their type and context *) +val new_evar : + evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr +(* the same with side-effects *) +val e_new_evar : + evar_defs ref -> env -> ?src:loc * hole_kind -> types -> constr + +(* Create a fresh evar in a context different from its definition context: + [new_evar_instance sign evd ty inst] creates a new evar of context + [sign] and type [ty], [inst] is a mapping of the evar context to + the context where the evar should occur. This means that the terms + of [inst] are typed in the occurrence context and their type (seen + as a telescope) is [sign] *) +val new_evar_instance : + named_context -> evar_defs -> types -> ?src:loc * hole_kind -> constr list -> + evar_defs * constr + +(* Builds the instance in the case where the occurrence context is the + same as the evar context *) +val make_evar_instance : env -> constr list -val new_isevar : evar_defs -> env -> loc * hole_kind -> constr -> - evar_defs * constr +(***********************************************************) -(* the same with side-effects *) -val e_new_isevar : evar_defs ref -> env -> loc * hole_kind -> constr -> constr +val non_instantiated : evar_map -> (evar * evar_info) list +val has_undefined_evars : evar_defs -> constr -> bool val is_eliminator : constr -> bool val head_is_embedded_evar : evar_defs -> constr -> bool val solve_simple_eqn : @@ -106,10 +96,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts (***********************************************************) (* Value/Type constraints *) -val new_Type_sort : unit -> sorts -val new_Type : unit -> constr val judge_of_new_Type : unit -> unsafe_judgment -val refresh_universes : types -> types type type_constraint = constr option type val_constraint = constr option diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d7468eded..c91d9ae7d 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -13,6 +13,7 @@ open Names open Term open Sign open Environ +open Libnames (* The type of mappings for existential variables *) @@ -60,6 +61,7 @@ let is_defined sigma ev = not (info.evar_body = Evar_empty) let evar_body ev = ev.evar_body +let evar_env evd = Global.env_of_context evd.evar_hyps let string_of_existential ev = "?" ^ string_of_int ev @@ -184,25 +186,103 @@ let metamap_to_list m = let metamap_inv m b = Metamap.fold (fun n v l -> if v = b then n::l else l) m [] +(*************************) +(* Unification state *) + +type hole_kind = + | ImplicitArg of global_reference * (int * identifier option) + | BinderType of name + | QuestionMark + | CasesType + | InternalHole + | TomatchTypeParameter of inductive * int + +type conv_pb = + | CONV + | CUMUL + type meta_map = clbinding Metamap.t - -let meta_defined env mv = - match Metamap.find mv env with +type evar_constraint = conv_pb * constr * constr +type evar_defs = + { evars : evar_map; + conv_pbs : evar_constraint list; + history : (existential_key * (loc * hole_kind)) list; + metas : meta_map } + +let mk_evar_defs (sigma,mmap) = + { evars=sigma; conv_pbs=[]; history=[]; metas=mmap } +let create_evar_defs sigma = + mk_evar_defs (sigma,Metamap.empty) +let evars_of d = d.evars +let metas_of d = d.metas +let evars_reset_evd evd d = {d with evars = evd} +let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} +let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} +let evar_source ev d = + try List.assoc ev d.history + with Failure _ -> (dummy_loc, InternalHole) + +(* define the existential of section path sp as the constr body *) +let evar_define sp body isevars = + (* needed only if an inferred type *) + let body = Termops.refresh_universes body in + {isevars with evars = define isevars.evars sp body} + + +let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd = + { evd with + evars = add evd.evars evn + {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty}; + history = (evn,src)::evd.history } + +let set_evar_source ev k evd = {evd with history=(ev,k)::evd.history} + +let is_defined_evar isevars (n,_) = is_defined isevars.evars n + +(* Does k corresponds to an (un)defined existential ? *) +let is_undefined_evar isevars c = match kind_of_term c with + | Evar ev -> not (is_defined_evar isevars ev) + | _ -> false + + +let get_conv_pbs isevars p = + let (pbs,pbs1) = + List.fold_left + (fun (pbs,pbs1) pb -> + if p pb then + (pb::pbs,pbs1) + else + (pbs,pb::pbs1)) + ([],[]) + isevars.conv_pbs + in + {isevars with conv_pbs = pbs1}, + pbs + +let meta_defined evd mv = + match Metamap.find mv evd.metas with | Clval _ -> true | Cltyp _ -> false -let meta_fvalue env mv = - match Metamap.find mv env with +let meta_fvalue evd mv = + match Metamap.find mv evd.metas with | Clval(b,_) -> b | Cltyp _ -> anomaly "meta_fvalue: meta has no value" -let meta_ftype env mv = - match Metamap.find mv env with +let meta_ftype evd mv = + match Metamap.find mv evd.metas with | Cltyp b -> b | Clval(_,b) -> b -let meta_declare mv v menv = - Metamap.add mv (Cltyp(mk_freelisted v)) menv +let meta_declare mv v evd = + { evd with metas = Metamap.add mv (Cltyp(mk_freelisted v)) evd.metas } -let meta_assign mv v menv = - Metamap.add mv (Clval(mk_freelisted v, meta_ftype menv mv)) menv +let meta_assign mv v evd = + {evd with + metas = + Metamap.add mv (Clval(mk_freelisted v, meta_ftype evd mv)) evd.metas } + +let meta_merge evd1 evd2 = + {evd2 with + metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) + evd2.metas (metamap_to_list evd1.metas) } diff --git a/pretyping/evd.mli b/pretyping/evd.mli index df362a9bf..fd6e944e1 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -9,9 +9,11 @@ (*i $Id$ i*) (*i*) +open Util open Names open Term open Sign +open Libnames (*i*) (* The type of mappings for existential variables. @@ -51,6 +53,7 @@ val is_evar : evar_map -> evar -> bool val is_defined : evar_map -> evar -> bool val evar_body : evar_info -> evar_body +val evar_env : evar_info -> Environ.env val string_of_existential : evar -> string val existential_of_int : int -> evar @@ -104,8 +107,51 @@ type clbinding = 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 + +(*************************) +(* Unification state *) + +type hole_kind = + | ImplicitArg of global_reference * (int * identifier option) + | BinderType of name + | QuestionMark + | CasesType + | InternalHole + | TomatchTypeParameter of inductive * int + +type conv_pb = + | CONV + | CUMUL + +type evar_defs +val evars_of : evar_defs -> evar_map +val metas_of : evar_defs -> meta_map + +val mk_evar_defs : evar_map * meta_map -> evar_defs +(* the same with empty meta map: *) +val create_evar_defs : evar_map -> evar_defs +val evars_reset_evd : evar_map -> evar_defs -> evar_defs +val reset_evd : evar_map * meta_map -> evar_defs -> evar_defs +val evar_source : existential_key -> evar_defs -> loc * hole_kind + +type evar_constraint = conv_pb * constr * constr +val add_conv_pb : evar_constraint -> evar_defs -> evar_defs + +val evar_declare : + named_context -> evar -> types -> ?src:loc * hole_kind -> + evar_defs -> evar_defs +val evar_define : evar -> constr -> evar_defs -> evar_defs + +val is_defined_evar : evar_defs -> existential -> bool +val is_undefined_evar : evar_defs -> constr -> bool + +val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> + evar_defs * evar_constraint list + +val meta_defined : evar_defs -> metavariable -> bool +val meta_fvalue : evar_defs -> metavariable -> constr freelisted +val meta_ftype : evar_defs -> metavariable -> constr freelisted +val meta_declare : metavariable -> types -> evar_defs -> evar_defs +val meta_assign : metavariable -> constr -> evar_defs -> evar_defs + +val meta_merge : evar_defs -> evar_defs -> evar_defs diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 84fd4798b..d3a602ac2 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -24,8 +24,8 @@ type pretype_error = | CantFindCaseType of constr (* Unification *) | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * hole_kind - | UnsolvableImplicit of hole_kind + | NotClean of existential_key * constr * Evd.hole_kind + | UnsolvableImplicit of Evd.hole_kind | CannotUnify of constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index fadd3f338..ee4cdb206 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -26,8 +26,8 @@ type pretype_error = | CantFindCaseType of constr (* Unification *) | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * hole_kind - | UnsolvableImplicit of hole_kind + | NotClean of existential_key * constr * Evd.hole_kind + | UnsolvableImplicit of Evd.hole_kind | CannotUnify of constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr @@ -84,9 +84,10 @@ val error_ill_typed_rec_body_loc : val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_not_clean : - env -> Evd.evar_map -> existential_key -> constr -> loc * hole_kind -> 'b + env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b -val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b +val error_unsolvable_implicit : + loc -> env -> Evd.evar_map -> Evd.hole_kind -> 'b val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d0402a552..0054c4770 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -276,7 +276,7 @@ let rec pretype tycon env isevars lvar = function | RHole (loc,k) -> (match tycon with | Some ty -> - { uj_val = e_new_isevar isevars env (loc,k) ty; uj_type = ty } + { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } | None -> error_unsolvable_implicit loc env (evars_of !isevars) k) | RRec (loc,fixkind,names,bl,lar,vdef) -> @@ -391,7 +391,7 @@ let rec pretype tycon env isevars lvar = function | RLetIn(loc,name,c1,c2) -> let j = pretype empty_tycon env isevars lvar c1 in - let t = Evarutil.refresh_universes j.uj_type in + let t = refresh_universes j.uj_type in let var = (name,Some j.uj_val,t) in let tycon = option_app (lift 1) tycon in let j' = pretype tycon (push_rel var env) isevars lvar c2 in @@ -529,7 +529,7 @@ let rec pretype tycon env isevars lvar = function Cases.pred_case_ml env (evars_of !isevars) false indt (0,fj.uj_type) in - if has_undefined_isevars !isevars pred then + if has_undefined_evars !isevars pred then use_constraint () else true, pred @@ -683,7 +683,8 @@ let rec pretype tycon env isevars lvar = function | None -> let p = match tycon with | Some ty -> ty - | None -> e_new_isevar isevars env (loc,InternalHole) (new_Type ()) + | None -> + e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let f cs b = @@ -750,7 +751,7 @@ let rec pretype tycon env isevars lvar = function let pred = Cases.pred_case_ml (* eta-expanse *) env (evars_of !isevars) isrec indt (i,fj.uj_type) in - if has_undefined_isevars !isevars pred then findtype (i+1) + if has_undefined_evars !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env (evars_of !isevars) pred in @@ -942,7 +943,7 @@ and pretype_type valcon env isevars lvar = function utj_type = s } | None -> let s = new_Type_sort () in - { utj_val = e_new_isevar isevars env loc (mkSort s); + { utj_val = e_new_evar isevars env ~src:loc (mkSort s); utj_type = s}) | c -> let j = pretype empty_tycon env isevars lvar c in diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 1aeca07cb..0a9722b87 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -15,6 +15,7 @@ open Sign open Term open Libnames open Nametab +open Evd (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -48,14 +49,6 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) - | BinderType of name - | QuestionMark - | CasesType - | InternalHole - | TomatchTypeParameter of inductive * int - type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 54bb306bd..ff1f86c58 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -46,14 +46,6 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) - | BinderType of name - | QuestionMark - | CasesType - | InternalHole - | TomatchTypeParameter of inductive * int - type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -74,7 +66,7 @@ type rawconstr = | RRec of loc * fix_kind * identifier array * rawdecl list array * rawconstr array * rawconstr array | RSort of loc * rawsort - | RHole of (loc * hole_kind) + | RHole of (loc * Evd.hole_kind) | RCast of loc * rawconstr * rawconstr | RDynamic of loc * Dyn.t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a9fc90df2..9372effeb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -461,10 +461,6 @@ let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; type conversion_test = constraints -> constraints -type conv_pb = - | CONV - | CUMUL - let pb_is_equal pb = pb = CONV let pb_equal = function diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b02cc4214..9c70b1a40 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -162,10 +162,6 @@ val reduce_fix : local_state_reduction_function -> fixpoint type conversion_test = constraints -> constraints -type conv_pb = - | CONV - | CUMUL - val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 18c54da47..f0c01a56e 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -9,12 +9,9 @@ (*i $Id$ i*) (*i*) -open Names open Term open Evd open Environ -open Pattern -open Termops (*i*) (* This family of functions assumes its constr argument is known to be @@ -23,11 +20,12 @@ open Termops either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -val get_type_of : env -> evar_map -> constr -> constr +val get_type_of : env -> evar_map -> constr -> types val get_sort_of : env -> evar_map -> types -> sorts val get_sort_family_of : env -> evar_map -> types -> sorts_family -val get_type_of_with_meta : env -> evar_map -> metamap -> constr -> constr +val get_type_of_with_meta : + env -> evar_map -> Termops.metamap -> constr -> types (* Makes an assumption from a constr *) val get_assumption_of : env -> evar_map -> constr -> types diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 02e8618dc..d8c85cf7a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -101,6 +101,20 @@ let new_univ = (fun sp -> incr univ_gen; Univ.make_univ (Lib.library_dp(),!univ_gen)) +let new_Type () = mkType (new_univ ()) +let new_Type_sort () = Type (new_univ ()) + +(* This refreshes universes in types; works only for inferred types (i.e. for + types of the form (x1:A1)...(xn:An)B with B a sort or an atom in + head normal form) *) +let refresh_universes t = + let modified = ref false in + let rec refresh t = match kind_of_term t with + | Sort (Type _) -> modified := true; new_Type () + | Prod (na,u,v) -> mkProd (na,u,refresh v) + | _ -> t in + let t' = refresh t in + if !modified then t' else t let new_sort_in_family = function | InProp -> mk_Prop diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 8ce7b39dc..e1a9d5ba9 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -19,6 +19,9 @@ open Environ (*val set_module : Names.dir_path -> unit*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts +val new_Type : unit -> types +val new_Type_sort : unit -> sorts +val refresh_universes : types -> types (* printers *) val print_sort : sorts -> std_ppcmds diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b98ff0e7d..9aa2758a0 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -24,23 +24,24 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) (* The typing machine without information, without universes but with existential variables. *) -let assumption_of_judgment env (sigma,_) j = - assumption_of_judgment env (j_nf_evar sigma j) +let assumption_of_judgment env evd j = + assumption_of_judgment env (j_nf_evar (Evd.evars_of evd) j) -let type_judgment env (sigma,_) j = - type_judgment env (j_nf_evar sigma j) +let type_judgment env evd j = + type_judgment env (j_nf_evar (Evd.evars_of evd) j) -let check_type env (sigma,_) j ty = +let check_type env evd j ty = + let sigma = Evd.evars_of evd in 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 env evd cstr = match kind_of_term cstr with | Meta n -> - { uj_val = cstr; uj_type = Evarutil.meta_type (snd evd) n } + { uj_val = cstr; uj_type = Evarutil.meta_type evd n } | Evar ev -> - let sigma = fst evd in + let sigma = Evd.evars_of 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 @@ -161,11 +162,11 @@ let msort_of env evd c = a.utj_type let type_of env sigma c = - mtype_of env (sigma, Evd.Metamap.empty) c + mtype_of env (Evd.create_evar_defs sigma) c let sort_of env sigma c = - msort_of env (sigma, Evd.Metamap.empty) c + msort_of env (Evd.create_evar_defs sigma) c let check env sigma c = - mcheck env (sigma, Evd.Metamap.empty) c + mcheck env (Evd.create_evar_defs sigma) c (* The typed type of a judgment. *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 15f3a6597..c4503f51b 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -25,9 +25,9 @@ val sort_of : env -> evar_map -> types -> sorts 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 +val mtype_of : env -> evar_defs -> constr -> types +val msort_of : env -> evar_defs -> types -> sorts +val mcheck : env -> evar_defs -> constr -> types -> unit (* unused typing function... *) -val mtype_of_type : env -> evar_map * meta_map -> types -> types +val mtype_of_type : env -> evar_defs -> types -> types diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 33f09fd0a..11b24f096 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -51,7 +51,7 @@ let abstract_list_all env sigma typ c l = let w_Declare env sp ty evd = let sigma = evars_of evd in - let _ = Typing.type_of env sigma ty in (* Utile ?? *) + let _ = Typing.type_of env sigma ty in (* Checks there is no meta *) let newdecl = { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in evars_reset_evd (Evd.add sigma sp newdecl) evd @@ -211,9 +211,7 @@ let applyHead env evd n c = else match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_isevar evd env - (dummy_loc,Rawterm.InternalHole) c1 in + let (evd',evar) = Evarutil.new_evar evd env c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in @@ -270,25 +268,23 @@ let w_merge env with_types metas evars evd = | _ -> anomaly "w_merge_rec")) | ([], (mv,n)::t) -> - let mmap = metas_of evd in - if meta_defined mmap mv then + if meta_defined evd mv then let (metas',evars') = - unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in + unify_0 env (evars_of evd) CONV (meta_fvalue evd mv).rebus n in w_merge_rec evd (metas'@t) evars' else begin if with_types (* or occur_meta mvty *) then - (let mvty = meta_type mmap mv in + (let mvty = meta_type evd mv in try let sigma = evars_of evd in (* why not typing with the metamap ? *) - let nty = Typing.type_of env sigma (nf_meta mmap n) in + let nty = Typing.type_of env sigma (nf_meta evd 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 -> ()); - let evd' = - reset_evd (evars_of evd,meta_assign mv n mmap) evd in + let evd' = meta_assign mv n evd in w_merge_rec evd' t [] end @@ -430,7 +426,7 @@ let secondOrderAbstraction env allow_K typ (p, oplist) evd = let sigma = evars_of evd in let (evd',cllist) = w_unify_to_subterm_list env allow_K oplist typ evd in - let typp = meta_type (metas_of evd') p in + let typp = meta_type evd' p in let pred = abstract_list_all env sigma typp typ cllist in w_unify_0 env CONV (mkMeta p) pred evd' @@ -443,13 +439,13 @@ let w_unify2 env allow_K cv_pb ty1 ty2 evd = let evd' = secondOrderAbstraction env allow_K ty2 (p1,oplist1) evd in (* Resume first order unification *) - w_unify_0 env cv_pb (nf_meta (metas_of evd') ty1) ty2 evd' + w_unify_0 env cv_pb (nf_meta evd' ty1) ty2 evd' | _, Meta p2 -> (* Find the predicate *) let evd' = secondOrderAbstraction env allow_K ty1 (p2, oplist2) evd in (* Resume first order unification *) - w_unify_0 env cv_pb ty1 (nf_meta (metas_of evd') ty2) evd' + w_unify_0 env cv_pb ty1 (nf_meta evd' ty2) evd' | _ -> error "w_unify2" diff --git a/pretyping/unification.mli b/pretyping/unification.mli index d3007e69d..95b35a56c 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -23,8 +23,7 @@ val w_Define : evar -> constr -> evar_defs -> evar_defs (* The "unique" unification fonction *) val w_unify : - bool -> env -> Reductionops.conv_pb -> constr -> constr -> - evar_defs -> evar_defs + bool -> env -> conv_pb -> constr -> constr -> evar_defs -> evar_defs (* [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 diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 41b910222..303338143 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -8,40 +8,13 @@ (* $Id$ *) -open Pp open Util open Names -open Rawterm open Term -open Termops -open Environ open Evd open Sign -open Reductionops -open Typing -open Tacred open Proof_trees -open Proof_type -open Logic open Refiner -open Tacexpr -open Nameops - - -type wc = named_context sigma (* for a better reading of the following *) - -let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it - -type w_tactic = named_context sigma -> named_context sigma - -let extract_decl sp evc = - let evdmap = evc.sigma in - let evd = Evd.map evdmap sp in - { it = evd.evar_hyps; - sigma = Evd.rmv evdmap sp } - -let restore_decl sp evd evc = - (rc_add evc (sp,evd)) (******************************************) (* Instantiation of existential variables *) @@ -49,34 +22,29 @@ let restore_decl sp evd evc = (* w_tactic pour instantiate *) -let w_refine ev rawc wc = - if Evd.is_defined wc.sigma ev then +let w_refine env ev rawc evd = + if Evd.is_defined (evars_of evd) ev then error "Instantiate called on already-defined evar"; - let e_info = Evd.map wc.sigma ev in - let env = Evarutil.evar_env e_info in - let evd,typed_c = - Pretyping.understand_gen_tcc wc.sigma env [] + let e_info = Evd.map (evars_of evd) ev in + let env = Evd.evar_env e_info in + let sigma,typed_c = + Pretyping.understand_gen_tcc (evars_of evd) env [] (Some e_info.evar_concl) rawc in let inst_info = {e_info with evar_body = Evar_defined typed_c } in - restore_decl ev inst_info (extract_decl ev {wc with sigma=evd}) - (* w_Define ev typed_c {wc with sigma=evd} *) - -(* the instantiate tactic was moved to tactics/evar_tactics.ml *) + evar_define ev typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in - let wc = project_with_focus gls in - let sigma = wc.sigma in - let (sp,evd) (* as evc *) = + let sigma = gls.sigma in + let (sp,evi) (* as evc *) = try List.nth (Evarutil.non_instantiated sigma) (n-1) with Failure _ -> - error "not so many uninstantiated existential variables" - in - let e_info = Evd.map sigma sp in - let env = Evarutil.evar_env e_info in + error "not so many uninstantiated existential variables" in + let env = Evd.evar_env evi in let rawc = Constrintern.interp_rawconstr sigma env com in - let wc' = w_refine sp rawc wc in - change_constraints_pftreestate wc'.sigma pfts + let evd = create_evar_defs sigma in + let evd' = w_refine env sp rawc evd in + change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 4766d94cb..57312cb4b 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -11,23 +11,14 @@ (*i*) open Names open Term -open Sign open Environ open Evd open Refiner -open Proof_type (*i*) -type wc = named_context sigma (* for a better reading of the following *) - (* Refinement of existential variables. *) -(* A [w_tactic] is a tactic which modifies the a set of evars of which - a goal depend, either by instantiating one, or by declaring a new - dependent goal *) -type w_tactic = wc -> wc - -val w_refine : evar -> Rawterm.rawconstr -> w_tactic +val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 967b3edaf..445e19967 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -70,25 +70,6 @@ let is_tactic_proof pf = match pf.ref with (* Constraints for existential variables *) (*******************************************************************) -(* A readable constraint is a global constraint plus a focus set - of existential variables and a signature. *) - -(* Functions on readable constraints *) - -let mt_evcty gc = - { it = empty_named_context; sigma = gc } - -let rc_of_gc evds gl = - { it = gl.evar_hyps; sigma = evds } - -let rc_add evc (k,v) = - { it = evc.it; - sigma = Evd.add evc.sigma k v } - -let get_hyps evc = evc.it -let get_env evc = Global.env_of_context evc.it -let get_gc evc = evc.sigma - let pf_lookup_name_as_renamed env ccl s = Detyping.lookup_name_as_renamed env ccl s diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 348a4b173..12f82b7f4 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -33,16 +33,6 @@ val is_complete_proof : proof_tree -> bool val is_leaf_proof : proof_tree -> bool val is_tactic_proof : proof_tree -> bool -(*s A readable constraint is a global constraint plus a focus set - of existential variables and a signature. *) - -val rc_of_gc : evar_map -> goal -> named_context sigma -val rc_add : named_context sigma -> existential_key * goal -> - named_context sigma -val get_hyps : named_context sigma -> named_context -val get_env : named_context sigma -> env -val get_gc : named_context sigma -> evar_map - val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option val pf_lookup_index_as_renamed : env -> constr -> int -> int option diff --git a/proofs/refiner.ml b/proofs/refiner.ml index b2629013b..acdc302af 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -31,8 +31,6 @@ let sig_it x = x.it let sig_sig x = x.sigma -let project_with_focus gls = rc_of_gc (gls.sigma) (gls.it) - let pf_status pf = pf.open_subgoals let is_complete pf = (0 = (pf_status pf)) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index f6f65ef93..8e39e0181 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -23,8 +23,6 @@ open Tacexpr val sig_it : 'a sigma -> 'a val sig_sig : 'a sigma -> evar_map -val project_with_focus : goal sigma -> named_context sigma - val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : diff --git a/tactics/equality.ml b/tactics/equality.ml index f9834f522..8dcc8e06b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -567,7 +567,7 @@ let minimal_free_rels env sigma (c,cty) = let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let { intro = exist_term } = find_sigma_data sort_of_ty in - let isevars = ref (Evarutil.create_evar_defs sigma) in + let isevars = ref (Evd.create_evar_defs sigma) in let rec sigrec_clausal_form siglen p_i = if siglen = 0 then if Evarconv.e_conv env isevars p_i dFLTty then @@ -579,19 +579,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let (a,p_i_minus_1) = match whd_beta_stack p_i with | (_sigS,[a;p]) -> (a,p) | _ -> anomaly "sig_clausal_form: should be a sigma type" in - let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole) - (Evarutil.new_Type ()) in + let ev = Evarutil.e_new_evar isevars env (new_Type ()) in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match - Evd.existential_opt_value (Evarutil.evars_of !isevars) + Evd.existential_opt_value (Evd.evars_of !isevars) (destEvar ev) with | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in - Evarutil.nf_evar (Evarutil.evars_of !isevars) scf + Evarutil.nf_evar (Evd.evars_of !isevars) scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index d65b1f3eb..a0be2149a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -20,7 +20,7 @@ open Termops (* The instantiate tactic *) -let evars_of evc c = +let evar_list evc c = let rec evrec acc c = match kind_of_term c with | Evar (n, _) when Evd.in_dom evc n -> c :: acc @@ -29,30 +29,30 @@ let evars_of evc c = evrec [] c let instantiate n rawc ido gl = - let wc = Refiner.project_with_focus gl in + let sigma = gl.sigma in let evl = match ido with - ConclLocation () -> evars_of wc.sigma gl.it.evar_concl + ConclLocation () -> evar_list sigma gl.it.evar_concl | HypLocation (id,hloc) -> let decl = lookup_named id gl.it.evar_hyps in match hloc with InHyp -> (match decl with - (_,None,typ) -> evars_of wc.sigma typ + (_,None,typ) -> evar_list sigma typ | _ -> error "please be more specific : in type or value ?") | InHypTypeOnly -> - let (_, _, typ) = decl in evars_of wc.sigma typ + let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> (match decl with - (_,Some body,_) -> evars_of wc.sigma body + (_,Some body,_) -> evar_list sigma body | _ -> error "not a let .. in hypothesis") in if List.length evl < n then error "not enough uninstantiated existential variables"; if n <= 0 then error "incorrect existential variable index"; let ev,_ = destEvar (List.nth evl (n-1)) in - let wc' = w_refine ev rawc wc in - Tacticals.tclIDTAC {gl with sigma = wc'.sigma} + let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma) in + Refiner.tclEVARS (evars_of evd') gl (* let pfic gls c = @@ -67,12 +67,9 @@ let instantiate_tac = function | _ -> invalid_arg "Instantiate called with bad arguments" *) -let let_evar nam typ gls = - let sp = Evarutil.new_evar () in - let evd = Evarutil.create_evar_defs gls.sigma in - let evd' = Unification.w_Declare (pf_env gls) sp typ evd in - let ngls = {gls with sigma = Evarutil.evars_of evd'} in - let args = Array.of_list - (List.map mkVar (ids_of_named_context (pf_hyps gls))) in - Tactics.forward true nam (mkEvar(sp,args)) ngls +let let_evar name typ gls = + let evd = Evd.create_evar_defs gls.sigma in + let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in + Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd')) + (Tactics.forward true name evar) gls diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 79aa71c0f..3d91877d0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -369,7 +369,7 @@ let general_elim_then_using match predicate with | None -> elimclause' | Some p -> - clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause' + clenv_unify true Evd.CONV (mkMeta pmv) p elimclause' in elim_res_pf_THEN_i elimclause' branchtacs gl diff --git a/toplevel/command.ml b/toplevel/command.ml index 33663ec21..6dad04c98 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -92,7 +92,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity) = let b = abstract_rawconstr com bl in let j = judgment_of_rawconstr sigma env b in { const_entry_body = j.uj_val; - const_entry_type = Some (Evarutil.refresh_universes j.uj_type); + const_entry_type = Some (refresh_universes j.uj_type); const_entry_opaque = opacity } | Some comtyp -> (* We use a cast to avoid troubles with evars in comtyp *) @@ -602,7 +602,7 @@ let build_scheme lnamedepindsort = let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in - let decltype = Evarutil.refresh_universes decltype in + let decltype = refresh_universes decltype in let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false } in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e032b9f00..8b1745bd3 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -27,6 +27,7 @@ open Logic open Printer open Ast open Rawterm +open Evd let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1b87853bd..2b2dc3138 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1039,7 +1039,7 @@ let vernac_check_guard () = let (pfterm,_) = extract_open_pftreestate pts in let message = try - Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf)) + Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf)) pfterm; (str "The condition holds up to here") with UserError(_,s) -> |