diff options
37 files changed, 378 insertions, 323 deletions
@@ -18,6 +18,9 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi: lib/pp.cmi kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi +kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \ + kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/sosub.cmi: kernel/term.cmi kernel/term.cmi: kernel/generic.cmi kernel/names.cmi lib/pp.cmi \ @@ -26,9 +29,6 @@ kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ kernel/term.cmi kernel/univ.cmi -kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/gmapl.cmi: lib/gmap.cmi lib/pp.cmi: lib/pp_control.cmi @@ -36,8 +36,8 @@ lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi library/global.cmi: kernel/constant.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/typing.cmi kernel/univ.cmi + kernel/inductive.cmi kernel/names.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/univ.cmi library/goptions.cmi: kernel/names.cmi library/impargs.cmi: kernel/names.cmi kernel/term.cmi library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \ @@ -89,6 +89,7 @@ pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ kernel/term.cmi pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi +pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ @@ -105,12 +106,12 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi kernel/term.cmi -proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ - kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi +proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi kernel/names.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi \ + kernel/term.cmi proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi -proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ lib/util.cmi @@ -206,6 +207,16 @@ kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmx \ kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmx \ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ kernel/univ.cmx lib/util.cmx kernel/reduction.cmi +kernel/safe_typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi kernel/indtypes.cmi kernel/inductive.cmi \ + kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi \ + lib/util.cmi kernel/safe_typing.cmi +kernel/safe_typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/generic.cmx kernel/indtypes.cmx kernel/inductive.cmx \ + kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \ + lib/util.cmx kernel/safe_typing.cmi kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi kernel/sign.cmi kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \ @@ -232,16 +243,6 @@ kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \ kernel/typeops.cmi -kernel/typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/generic.cmi kernel/indtypes.cmi kernel/inductive.cmi \ - kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi kernel/typing.cmi -kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/generic.cmx kernel/indtypes.cmx kernel/inductive.cmx \ - kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx kernel/typing.cmi kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi lib/bij.cmo: lib/gmap.cmi lib/bij.cmi @@ -287,12 +288,12 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \ library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ library/declare.cmi library/global.cmo: kernel/environ.cmi kernel/generic.cmi \ - kernel/inductive.cmi kernel/instantiate.cmi kernel/sign.cmi \ - library/summary.cmi kernel/term.cmi kernel/typing.cmi lib/util.cmi \ + kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \ library/global.cmi library/global.cmx: kernel/environ.cmx kernel/generic.cmx \ - kernel/inductive.cmx kernel/instantiate.cmx kernel/sign.cmx \ - library/summary.cmx kernel/term.cmx kernel/typing.cmx lib/util.cmx \ + kernel/inductive.cmx kernel/instantiate.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \ library/global.cmi library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \ lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi @@ -301,11 +302,11 @@ library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \ library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi kernel/inductive.cmi kernel/names.cmi \ kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ - kernel/typing.cmi library/impargs.cmi + library/impargs.cmi library/impargs.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx kernel/inductive.cmx kernel/names.cmx \ kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ - kernel/typing.cmx library/impargs.cmi + library/impargs.cmi library/indrec.cmo: kernel/environ.cmi kernel/generic.cmi \ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ @@ -410,22 +411,22 @@ pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \ proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \ - pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ + pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ pretyping/coercion.cmi pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/evarconv.cmx kernel/evd.cmx kernel/generic.cmx kernel/names.cmx \ - pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ + pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmi \ + kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/coercion.cmi pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarutil.cmi kernel/generic.cmi kernel/instantiate.cmi \ kernel/names.cmi pretyping/recordops.cmi kernel/reduction.cmi \ - kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi pretyping/evarconv.cmi + kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/evarutil.cmx kernel/generic.cmx kernel/instantiate.cmx \ kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \ - kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx pretyping/evarconv.cmi + kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \ @@ -434,8 +435,12 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \ pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi -pretyping/pretype_errors.cmo: kernel/names.cmi pretyping/pretype_errors.cmi -pretyping/pretype_errors.cmx: kernel/names.cmx pretyping/pretype_errors.cmi +pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi kernel/type_errors.cmi \ + pretyping/pretype_errors.cmi +pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \ + pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \ + pretyping/pretype_errors.cmi pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \ pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \ pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \ @@ -462,32 +467,40 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \ library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/recordops.cmi +pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ + kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi +pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ + kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \ + kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/clenv.cmi + pretyping/pretyping.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \ + proofs/clenv.cmi proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/clenv.cmi + pretyping/pretyping.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \ + proofs/clenv.cmi proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/evar_refiner.cmi + pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/evar_refiner.cmi + pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/typeops.cmi kernel/typing.cmi proofs/typing_ev.cmi \ - lib/util.cmi proofs/logic.cmi + kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/logic.cmi proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx proofs/typing_ev.cmx \ - lib/util.cmx proofs/logic.cmi + kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/logic.cmi proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \ @@ -498,10 +511,10 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/proof_trees.cmi + pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi proofs/proof_trees.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/names.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/proof_trees.cmi + pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi proofs/refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ @@ -516,18 +529,18 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \ proofs/tacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx proofs/macros.cmx \ kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \ kernel/term.cmx lib/util.cmx proofs/tacinterp.cmi -proofs/tacmach.cmo: parsing/ast.cmi kernel/environ.cmi \ +proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ kernel/sign.cmi lib/stamps.cmi proofs/tacred.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/tacmach.cmi -proofs/tacmach.cmx: parsing/ast.cmx kernel/environ.cmx \ + pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi +proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/tacmach.cmi + pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi proofs/tacred.cmo: kernel/closure.cmi library/declare.cmi kernel/environ.cmi \ kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \ kernel/names.cmi lib/pp.cmi library/redinfo.cmi kernel/reduction.cmi \ @@ -536,12 +549,6 @@ proofs/tacred.cmx: kernel/closure.cmx library/declare.cmx kernel/environ.cmx \ kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \ kernel/names.cmx lib/pp.cmx library/redinfo.cmx kernel/reduction.cmx \ kernel/term.cmx lib/util.cmx proofs/tacred.cmi -proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ - kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ - kernel/typeops.cmi lib/util.cmi proofs/typing_ev.cmi -proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ - kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \ - kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \ tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \ tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \ @@ -549,7 +556,7 @@ tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \ tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacinterp.cmi tactics/auto.cmi tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ tactics/dhyp.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \ @@ -558,7 +565,7 @@ tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ tactics/pattern.cmx proofs/pfedit.cmi lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/auto.cmi tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \ tactics/btermdn.cmi @@ -664,12 +671,12 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \ kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \ - kernel/names.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typing.cmi lib/util.cmi + kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \ kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \ - kernel/names.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typing.cmx lib/util.cmx + kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx lib/util.cmx toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ toplevel/vernacinterp.cmi toplevel/mltop.cmi @@ -706,7 +713,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \ proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ library/states.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \ - kernel/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + pretyping/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \ kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \ @@ -715,7 +722,7 @@ toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ proofs/pfedit.cmi lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ library/states.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \ - kernel/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi + pretyping/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ @@ -42,24 +42,14 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \ kernel/closure.cmo kernel/reduction.cmo \ kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ - kernel/typing.cmo + kernel/safe_typing.cmo LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ library/global.cmo library/states.cmo library/library.cmo \ library/nametab.cmo library/impargs.cmo library/redinfo.cmo \ library/indrec.cmo library/declare.cmo -PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \ - proofs/proof_trees.cmo proofs/logic.cmo \ - proofs/refiner.cmo proofs/evar_refiner.cmo \ - proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo - -TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ - tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ - tactics/wcclausenv.cmo tactics/tacticals.cmo \ - tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo - -PRETYPING=pretyping/classops.cmo pretyping/recordops.cmo \ +PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ pretyping/pretype_errors.cmo pretyping/coercion.cmo \ pretyping/multcase.cmo pretyping/pretyping.cmo @@ -69,6 +59,16 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\ parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo +PROOFS=proofs/tacred.cmo \ + proofs/proof_trees.cmo proofs/logic.cmo \ + proofs/refiner.cmo proofs/evar_refiner.cmo \ + proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo + +TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ + tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ + tactics/wcclausenv.cmo tactics/tacticals.cmo \ + tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo + TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/vernac.cmo toplevel/mltop.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo @@ -76,15 +76,15 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) -CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(TACTICS) \ - $(PRETYPING) $(PARSING) $(TOPLEVEL) +CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ + $(PROOFS) $(TACTICS) $(TOPLEVEL) CMX=$(CMO:.cmo=.cmx) # Targets world: minicoq coqtop.byte dev/db_printers.cmo -LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(PRETYPING) +LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(PRETYPING) # $(PROOFS) $(TACTICS) $(TOPLEVEL) link: $(LINK) ocamlc -o link $(LINK) diff --git a/kernel/environ.ml b/kernel/environ.ml index ccf3e1e20c..bed45797d8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,6 +43,7 @@ let empty_env = { let universes env = env.env_universes let context env = env.env_context +let var_context env = let (ENVIRON(g,_)) = env.env_context in g (* Construction functions. *) @@ -50,8 +51,8 @@ let push_var idvar env = { env with env_context = add_glob idvar env.env_context } let change_hyps f env = - let ctx = env.env_context in - { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) } + let (ENVIRON(g,r)) = env.env_context in + { env with env_context = ENVIRON (f g, r) } let push_rel idrel env = { env with env_context = add_rel idrel env.env_context } diff --git a/kernel/environ.mli b/kernel/environ.mli index d3fd22c01e..9f1c228a00 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -22,6 +22,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val var_context : unsafe_env -> var_context val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val change_hyps : diff --git a/kernel/evd.ml b/kernel/evd.ml index dd387ddfb4..4599fbdc43 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -65,7 +65,7 @@ let is_defined sigma ev = let info = map sigma ev in not (info.evar_body = Evar_empty) -let evar_hyps ev = get_globals (context ev.evar_env) +let evar_hyps ev = var_context ev.evar_env let id_of_existential ev = id_of_string ("?" ^ string_of_int ev) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 96fe8d5846..00e8a442bb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -244,7 +244,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = let packets = Array.of_list (list_map_i one_packet 1 inds) in { mind_kind = kind; mind_ntypes = ntypes; - mind_hyps = get_globals (context env); + mind_hyps = var_context env; mind_packets = packets; mind_constraints = cst; mind_singl = None; diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4bc551c6aa..2ce121ed12 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables * Similarly we have is_fmachine1_metas and is_resolve1_metas *) -let rec whd_ise1_metas env sigma = function +let rec whd_ise1_metas sigma = function | (DOPN(Evar n,_) as k) -> if Evd.in_dom sigma n then if Evd.is_defined sigma n then - whd_ise1_metas env sigma (existential_value sigma k) + whd_ise1_metas sigma (existential_value sigma k) else let m = DOP0(Meta (new_meta())) in DOP2(Cast,m,existential_type sigma k) else k - | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c + | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c diff --git a/kernel/typing.ml b/kernel/safe_typing.ml index db3d00302e..e523be5108 100644 --- a/kernel/typing.ml +++ b/kernel/safe_typing.ml @@ -233,6 +233,7 @@ let empty_environment = empty_env let universes = universes let context = context +let var_context = var_context let lookup_var = lookup_var let lookup_rel = lookup_rel @@ -283,7 +284,7 @@ let add_constant sp ce env = const_kind = kind_of_path sp; const_body = Some ce.const_entry_body; const_type = ty; - const_hyps = get_globals (context env); + const_hyps = var_context env; const_constraints = Constraint.union cst cst'; const_opaque = false } in @@ -296,7 +297,7 @@ let add_parameter sp t env = const_kind = kind_of_path sp; const_body = None; const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = get_globals (context env); + const_hyps = var_context env; const_constraints = cst; const_opaque = false } in diff --git a/kernel/typing.mli b/kernel/safe_typing.mli index 10530d123b..392040814f 100644 --- a/kernel/typing.mli +++ b/kernel/safe_typing.mli @@ -24,6 +24,7 @@ val empty_environment : environment val universes : environment -> universes val context : environment -> context +val var_context : environment -> var_context val push_var : identifier * constr -> environment -> environment val push_rel : name * constr -> environment -> environment diff --git a/kernel/sign.ml b/kernel/sign.ml index 5d7d5309b0..0b34c7edf3 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -10,7 +10,7 @@ open Term type 'a signature = identifier list * 'a list type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature let gLOB hyps = ENVIRON (hyps,[]) @@ -233,7 +233,7 @@ let lookup_id id env = | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature diff --git a/kernel/sign.mli b/kernel/sign.mli index 2a0a567dec..e2ef7d4a1e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term (*s Signatures with named and de Bruijn variables. *) type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature - -val gLOB : 'b signature -> ('b,'a) env - -val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env -val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env -val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b) -val lookup_rel : int -> ('b,'a) env -> (name * 'a) -val mem_glob : identifier -> ('b,'a) env -> bool - -val get_globals : ('b,'a) env -> 'b signature -val get_rels : ('b,'a) env -> 'a db_signature -val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c -val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c -val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env -val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env -val isnull_rel_env : ('a,'b) env -> bool -val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env -val ids_of_env : ('a, 'b) env -> identifier list +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature + +val gLOB : 'b signature -> ('b,'a) sign + +val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign +val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign +val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b) +val lookup_rel : int -> ('b,'a) sign -> (name * 'a) +val mem_glob : identifier -> ('b,'a) sign -> bool + +val get_globals : ('b,'a) sign -> 'b signature +val get_rels : ('b,'a) sign -> 'a db_signature +val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c +val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c +val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign +val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign +val isnull_rel_env : ('a,'b) sign -> bool +val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign +val ids_of_env : ('a, 'b) sign -> identifier list type ('b,'a) search_result = | GLOBNAME of identifier * 'b | RELNAME of int * 'a -val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result +val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature val unitize_env : 'a assumptions -> unit assumptions diff --git a/kernel/typeops.ml b/kernel/typeops.ml index d224b0209e..0d2d5cba50 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) = current context of [env]. *) let construct_reference id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if hyps_inclusion env sigma hyps hyps' then Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) else error_reference_variables CCI env id let check_hyps id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id @@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind = let type_of_existential env sigma c = let (ev,args) = destEvar c in let evi = Evd.map sigma ev in - let hyps = get_globals (context evi.Evd.evar_env) in + let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in check_hyps id env sigma hyps; instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) diff --git a/library/declare.ml b/library/declare.ml index 5d7d624121..0dcdf3dd28 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -213,7 +213,7 @@ let global_operator sp id = let global_reference kind id = let sp = Nametab.sp_of_id kind id in let (oper,_) = global_operator sp id in - let hyps = get_globals (Global.context ()) in + let hyps = Global.var_context () in let ids = ids_of_sign hyps in DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) diff --git a/library/global.ml b/library/global.ml index 9238b6e85c..0fc1852cb9 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ open Generic open Term open Instantiate open Sign -open Typing +open Safe_typing open Summary (* We introduce here the global environment of the system, and we declare it @@ -28,6 +28,7 @@ let _ = let universes () = universes !global_env let context () = context !global_env +let var_context () = var_context !global_env let push_var idc = global_env := push_var idc !global_env let push_rel nac = global_env := push_rel nac !global_env diff --git a/library/global.mli b/library/global.mli index 22623424bb..3e557b350b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -9,7 +9,7 @@ open Sign open Constant open Inductive open Environ -open Typing +open Safe_typing (*i*) (* This module defines the global environment of Coq. @@ -21,6 +21,7 @@ val unsafe_env : unit -> unsafe_env val universes : unit -> universes val context : unit -> context +val var_context : unit -> var_context val push_var : identifier * constr -> unit val push_rel : name * constr -> unit diff --git a/library/impargs.ml b/library/impargs.ml index a8fe59cc80..8fe93b97c1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -7,7 +7,6 @@ open Term open Reduction open Constant open Inductive -open Typing type implicits = | Impl_auto of int list @@ -18,7 +17,7 @@ let implicit_args = ref false let auto_implicits ty = if !implicit_args then - let genv = unsafe_env_of_env (Global.env()) in + let genv = Global.unsafe_env() in Impl_auto (poly_args genv Evd.empty ty) else No_impl diff --git a/parsing/astterm.ml b/parsing/astterm.ml index fddb478045..f2befc1d26 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -615,7 +615,7 @@ let ast_adjust_consts sigma = (* locations are kept *) let globalize_command ast = let env = Global.unsafe_env () in - let sign = get_globals (Environ.context env) in + let sign = Environ.var_context env in ast_adjust_consts Evd.empty (gLOB sign) ast (* Avoid globalizing in non command ast for tactics *) @@ -633,8 +633,7 @@ let rec glob_ast sigma env = function | x -> x let globalize_ast ast = - let env = Global.unsafe_env () in - let sign = get_globals (Environ.context env) in + let sign = Global.var_context () in glob_ast Evd.empty (gLOB sign) ast diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 0588446225..ea83e68b1f 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -42,7 +42,7 @@ let print_basename_mind sp mindid = let print_closed_sections = ref false let print_typed_value_in_env env (trm,typ) = - let sign = get_globals (Environ.context env) in + let sign = Environ.var_context env in [< term0 (gLOB sign) trm ; 'fNL ; 'sTR " : "; term0 (gLOB sign) typ ; 'fNL >] @@ -352,7 +352,7 @@ let print_constructors_rel fn mip = List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid let crible (fn:string -> unit assumptions -> constr -> unit) name = - let hyps = gLOB (get_globals (Global.context())) in + let hyps = gLOB (Global.var_context()) in let imported = Library.opened_modules() in let const = global_reference CCI name in let rec crible_rec = function @@ -438,7 +438,7 @@ let print_name name = let print_opaque_name name = let sigma = Evd.empty in let env = Global.unsafe_env () in - let sign = get_globals (Global.context ()) in + let sign = Global.var_context () in try match global_reference CCI name with | DOPN(Const sp,_) as x -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7959b5c7c2..f7096f2682 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,64 +1,77 @@ (* $Id$ *) -open Util;; -open Generic;; -open Names;; -open Term;; -open Reduction;; -open Environ;; -open Typeops;; -open Type_errors;; -open Classops;; -open Recordops;; -open Evarconv;; +open Util +open Generic +open Names +open Term +open Reduction +open Environ +open Typeops +open Type_errors +open Classops +open Recordops +open Evarconv +open Retyping (* Typing operations dealing with coercions *) -let class_of1 env sigma t = class_of sigma (nf_ise1 env sigma t);; +let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t) let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} + { uj_val = nf_ise1 sigma v; + uj_type = nf_ise1 sigma t; + uj_kind = k } + let jl_nf_ise env sigma = List.map (j_nf_ise env sigma) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function - [] -> {uj_val=applist(j_val_only funj,argl); - uj_type= typ; - uj_kind = funj.uj_kind} + | [] -> { uj_val=applist(j_val_only funj,argl); + uj_type= typ; + uj_kind = funj.uj_kind } | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) - match whd_betadeltaiota env Evd.empty typ with - DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" - in apply_rec [] funj.uj_type argl;; + (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) + match whd_betadeltaiota env Evd.empty typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + (* Typage garanti par l'appel a app_coercion*) + apply_rec (h::acc) (subst1 h c2) restl + | _ -> anomaly "apply_coercion_args" + in + apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions p a` hj *) let apply_pcoercion env p hj typ_cl = - if !compter then - (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p)); - try fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,b= coe_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if b then {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} - else jres),jres.uj_type) - (hj,typ_cl) p) - with _ -> failwith "apply_pcoercion" + if !compter then begin + nbpathc := !nbpathc +1; + nbcoer := !nbcoer + (List.length p) + end; + try + fst (List.fold_left + (fun (ja,typ_cl) i -> + let fv,b= coe_value i in + let argl = (class_args_of typ_cl)@[ja.uj_val] in + let jres = apply_coercion_args env argl fv in + (if b then + {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} + else + jres), + jres.uj_type) + (hj,typ_cl) p) + with _ -> + failwith "apply_pcoercion" let inh_app_fun env isevars j = - match whd_betadeltaiota env !isevars j.uj_type with - DOP2(Prod,_,DLAM(_,_)) -> j - | _ -> - (try - let t,i1 = class_of1 env !isevars j.uj_type in - let p = lookup_path_to_fun_from i1 in - apply_pcoercion env p j t - with _ -> j) + match whd_betadeltaiota env !isevars j.uj_type with + | DOP2(Prod,_,DLAM(_,_)) -> j + | _ -> + (try + let t,i1 = class_of1 env !isevars j.uj_type in + let p = lookup_path_to_fun_from i1 in + apply_pcoercion env p j t + with _ -> j) (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *) let inh_tosort_force env isevars j = @@ -69,110 +82,126 @@ let inh_tosort_force env isevars j = let inh_tosort env isevars j = let typ = whd_betadeltaiota env !isevars j.uj_type in match typ with - DOP0(Sort(_)) -> j (* idem inh_app_fun *) - | _ -> (try inh_tosort_force env isevars j with _ -> j) + | DOP0(Sort(_)) -> j (* idem inh_app_fun *) + | _ -> (try inh_tosort_force env isevars j with _ -> j) let inh_ass_of_j env isevars j = - let typ = whd_betadeltaiota env !isevars j.uj_type in - match typ with - DOP0(Sort s) -> {body=j.uj_val;typ=s} - | _ -> - (try - let j1 = inh_tosort_force env isevars j - in assumption_of_judgment env !isevars j1 - with _ -> error_assumption CCI env (nf_ise1 env !isevars j.uj_val)) - (* try ... with _ -> ... is BAD *) + let typ = whd_betadeltaiota env !isevars j.uj_type in + match typ with + | DOP0(Sort s) -> {body=j.uj_val;typ=s} + | _ -> + (try + let j1 = inh_tosort_force env isevars j in + assumption_of_judgment env !isevars j1 + with _ -> + error_assumption CCI env (nf_ise1 !isevars j.uj_val)) + (* try ... with _ -> ... is BAD *) let inh_coerce_to1 env isevars c1 v t k = - let t1,i1 = class_of1 env !isevars c1 in - let t2,i2 = class_of1 env !isevars t in - let p = lookup_path_between (i2,i1) in - let hj = {uj_val=v;uj_type=t;uj_kind=k} in - let hj' = apply_pcoercion env p hj t2 in - if the_conv_x_leq env isevars hj'.uj_type c1 then hj' - else failwith "inh_coerce_to" + let t1,i1 = class_of1 env !isevars c1 in + let t2,i2 = class_of1 env !isevars t in + let p = lookup_path_between (i2,i1) in + let hj = {uj_val=v;uj_type=t;uj_kind=k} in + let hj' = apply_pcoercion env p hj t2 in + if the_conv_x_leq env isevars hj'.uj_type c1 then + hj' + else + failwith "inh_coerce_to" let inh_coerce_to env isevars c1 hj = inh_coerce_to1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind - + let rec inh_conv_coerce1 env isevars c1 v t k = - if the_conv_x_leq env isevars t c1 - then {uj_val=v; uj_type=t; uj_kind=k} - else try inh_coerce_to1 env isevars c1 v t k - with _ -> (* try ... with _ -> ... is BAD *) - -(* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) - (match (whd_betadeltaiota env !isevars t, - whd_betadeltaiota env !isevars c1) with - | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> -(* let v' = hnf_constr !isevars v in*) - let v' = whd_betadeltaiota env !isevars v in - if (match v' with - DOP2(Lambda,v1,DLAM(_,v2)) -> - the_conv_x env isevars v1 u1 (* leq v1 u1? *) - | _ -> false) - then - let (x,v1,v2) = destLambda v' in -(* let jv1 = exemeta_rec def_vty_con env isevars v1 in - let assv1 = assumption_of_judgement env !isevars jv1 in - *) - let assv1 = outcast_type v1 in - let env1 = push_rel (x,assv1) env in - let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars x assv1 h2 - else -(* - let ju1 = exemeta_rec def_vty_con env isevars u1 in - let assu1 = assumption_of_judgement env !isevars ju1 in - *) - let assu1 = outcast_type u1 in - let name = (match name with Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = add_rel (name,assu1) env in - let h1 = - inh_conv_coerce1 env isevars1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in - let h2 = inh_conv_coerce1 env isevars1 u2 - (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) - (subst1 h1.uj_val t2) - (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars name assu1 h2 - | _ -> failwith "inh_coerce_to") + if the_conv_x_leq env isevars t c1 then + {uj_val=v; uj_type=t; uj_kind=k} + else + try + inh_coerce_to1 env isevars c1 v t k + with _ -> (* try ... with _ -> ... is BAD *) + (* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) + (match (whd_betadeltaiota env !isevars t, + whd_betadeltaiota env !isevars c1) with + | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> + (* let v' = hnf_constr !isevars v in *) + let v' = whd_betadeltaiota env !isevars v in + if (match v' with + | DOP2(Lambda,v1,DLAM(_,v2)) -> + the_conv_x env isevars v1 u1 (* leq v1 u1? *) + | _ -> false) + then + let (x,v1,v2) = destLambda v' in + (* let jv1 = exemeta_rec def_vty_con env isevars v1 in + let assv1 = assumption_of_judgement env !isevars jv1 in *) + let assv1 = outcast_type v1 in + let env1 = push_rel (x,assv1) env in + let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 + (mkSort (get_sort_of env !isevars t2)) in + abs_rel env !isevars x assv1 h2 + else + (* let ju1 = exemeta_rec def_vty_con env isevars u1 in + let assu1 = assumption_of_judgement env !isevars ju1 in *) + let assu1 = outcast_type u1 in + let name = (match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name) in + let env1 = push_rel (name,assu1) env in + let h1 = + inh_conv_coerce1 env isevars t1 (Rel 1) u1 + (mkSort (level_of_type assu1)) in + let h2 = inh_conv_coerce1 env isevars1 u2 + (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) + (subst1 h1.uj_val t2) + (mkSort (sort_of env !isevars1 t2)) + in + abs_rel !isevars name assu1 h2 + | _ -> failwith "inh_coerce_to") let inh_conv_coerce env isevars c1 hj = inh_conv_coerce1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind let inh_cast_rel env isevars cj tj = - let cj' = (try inh_conv_coerce env isevars tj.uj_val cj - with Not_found | Failure _ -> error_actual_type CCI env - (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in - { uj_val = mkCast cj'.uj_val tj.uj_val; - uj_type = tj.uj_val; - uj_kind = whd_betadeltaiota env !isevars tj.uj_type} + let cj' = + try + inh_conv_coerce env isevars tj.uj_val cj + with Not_found | Failure _ -> + error_actual_type CCI env + (j_nf_ise !isevars cj) (j_nf_ise !isevars tj) + in + { uj_val = mkCast cj'.uj_val tj.uj_val; + uj_type = tj.uj_val; + uj_kind = whd_betadeltaiota env !isevars tj.uj_type } let inh_apply_rel_list nocheck env isevars argjl funj vtcon = let rec apply_rec acc typ = function - [] -> let resj = - {uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); - uj_type= typ; - uj_kind = funj.uj_kind} in - (match vtcon with - | (_,(_,Some typ')) -> - (try inh_conv_coerce env isevars typ' resj - with _ -> resj) (* try ... with _ -> ... is BAD *) - | (_,(_,None)) -> resj) - - | hj::restjl -> - match whd_betadeltaiota env !isevars typ with - DOP2(Prod,c1,DLAM(_,c2)) -> - let hj' = - if nocheck then hj else - (try inh_conv_coerce env isevars c1 hj - with (Failure _ | Not_found) -> - error_cant_apply "Type Error" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in - apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl - | _ -> - error_cant_apply "Non-functional construction" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) - in apply_rec [] funj.uj_type argjl -;; + | [] -> + let resj = + { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); + uj_type= typ; + uj_kind = funj.uj_kind } + in + (match vtcon with + | (_,(_,Some typ')) -> + (try inh_conv_coerce env isevars typ' resj + with _ -> resj) (* try ... with _ -> ... is BAD *) + | (_,(_,None)) -> resj) + + | hj::restjl -> + match whd_betadeltaiota env !isevars typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + let hj' = + if nocheck then + hj + else + (try + inh_conv_coerce env isevars c1 hj + with Failure _ | Not_found -> + error_cant_apply "Type Error" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) + in + apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl + | _ -> + error_cant_apply "Non-functional construction" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) + in + apply_rec [] funj.uj_type argjl + diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cd9e6d9211..5af5fb9156 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -8,7 +8,7 @@ open Term open Reduction open Instantiate open Environ -open Typing_ev +open Typing open Classops open Recordops open Evarutil diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 43653f80d4..226b6ff0de 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -45,7 +45,7 @@ let filter_sign p sign x = (* All ids of sign must be distincts! *) let new_isevar_sign env sigma typ args = - let sign = get_globals (context env) in + let sign = var_context env in if not (list_distinct (ids_of_sign sign)) then error "new_isevar_sign: two vars have the same name"; let newev = Evd.new_evar() in @@ -60,7 +60,7 @@ let dummy_sort = mkType dummy_univ (* 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 sign = get_globals (context env) in + let sign = var_context env in let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in let (sigma',c) = new_isevar_sign env sigma dummy_sort args in (sigma', make_typed c (Type dummy_univ)) @@ -70,7 +70,7 @@ let split_evar_to_arrow sigma c = let evd = Evd.map sigma ev in let evenv = evd.evar_env in let (sigma1,dom) = new_type_var evenv sigma in - let hyps = get_globals (context evenv) in + let hyps = var_context evenv in let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in let nevenv = push_var (nvar,dom) evenv in let (sigma2,rng) = new_type_var nevenv sigma1 in @@ -97,7 +97,7 @@ let do_restrict_hyps sigma c = let args = Array.to_list args in let evd = Evd.map sigma ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,(rsign,ncargs)) = List.fold_left (fun (sign,(rs,na)) a -> @@ -244,7 +244,7 @@ let evar_define isevars lhs rhs = let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit) (Array.to_list argsv) in let evd = ise_map isevars ev in - let hyps = get_globals (context evd.evar_env) in + let hyps = var_context evd.evar_env in (* the substitution to invert *) let worklist = List.combine (ids_of_sign hyps) args in let body = real_clean isevars ev worklist rhs in @@ -263,7 +263,7 @@ let solve_refl conv_algo isevars c1 c2 = and (_,argsv2) = destEvar c2 in let evd = Evd.map !isevars ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,rsign) = array_fold_left2 (fun (sgn,rsgn) a1 a2 -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1e6245a471..500e6bfe74 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -146,17 +146,17 @@ let mt_evd = Evd.empty let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) -let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} +let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} = + {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k} -let jv_nf_ise env sigma = Array.map (j_nf_ise env sigma) +let jv_nf_ise sigma = Array.map (j_nf_ise sigma) (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) (* et autoriser des ? à rester dans le résultat de l'unification *) -let has_ise env sigma t = - try let _ = whd_ise env sigma t in true +let has_ise sigma t = + try let _ = whd_ise sigma t in true with UserError _ -> false let evar_type_fixpoint env isevars lna lar vdefj = @@ -166,8 +166,8 @@ let evar_type_fixpoint env isevars lna lar vdefj = if not (the_conv_x_leq env isevars (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then error_ill_typed_rec_body CCI env i lna - (jv_nf_ise env !isevars vdefj) - (Array.map (typed_app (nf_ise1 env !isevars)) lar) + (jv_nf_ise !isevars vdefj) + (Array.map (typed_app (nf_ise1 !isevars)) lar) done @@ -183,7 +183,7 @@ let cast_rel isevars env cj tj = let let_path = make_path ["Core"] (id_of_string "let") CCI let wrong_number_of_cases_message loc env isevars (c,ct) expn = - let c = nf_ise1 env !isevars c and ct = nf_ise1 env !isevars ct in + let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in error_number_branches_loc loc CCI env c ct expn let check_branches_message loc env isevars (c,ct) (explft,lft) = @@ -191,10 +191,11 @@ let check_branches_message loc env isevars (c,ct) (explft,lft) = if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn; for i = 0 to n-1 do if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then - let c = nf_ise1 env !isevars c - and ct = nf_ise1 env !isevars ct - and lfi = nf_betaiota env !isevars (nf_ise1 env !isevars lft.(i)) in - error_ill_formed_branch_loc loc CCI env c i lfi (nf_betaiota env !isevars explft.(i)) + let c = nf_ise1 !isevars c + and ct = nf_ise1 !isevars ct + and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in + error_ill_formed_branch_loc loc CCI env c i lfi + (nf_betaiota env !isevars explft.(i)) done (* @@ -287,10 +288,10 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let (valc,typc) = destCast v in {uj_val=valc; uj_type=typc; uj_kind=dummy_sort} | (false,(None,Some ty)) -> - let (c,ty) = new_isevar env isevars ty CCI in + let (c,ty) = new_isevar isevars env ty CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (true,(None,None)) -> - let (c,ty) = new_isevar env isevars (mkCast dummy_sort dummy_sort) CCI in + let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (false,(None,None)) -> (match loc with @@ -336,19 +337,20 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let j = pretype mt_tycon env isevars f in let j = inh_app_fun env isevars j in let apply_one_arg (tycon,jl) c = - let cj = pretype (app_dom_tycon isevars tycon) env isevars c in - let rtc = app_rng_tycon isevars cj.uj_val tycon in + let cj = pretype (app_dom_tycon env isevars tycon) env isevars c in + let rtc = app_rng_tycon env isevars cj.uj_val tycon in (rtc,cj::jl) in let jl = List.rev (snd (List.fold_left apply_one_arg (mk_tycon j.uj_type,[]) args)) in inh_apply_rel_list !trad_nocheck env isevars jl j vtcon | RBinder(loc,BLambda,name,c1,c2) -> - let j = pretype (abs_dom_valcon isevars vtcon) env isevars c1 in + let j = pretype (abs_dom_valcon env isevars vtcon) env isevars c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assum) in let j' = - pretype (abs_rng_tycon isevars vtcon) (push_rel var env) isevars c2 in + pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars c2 + in fst (abs_rel env !isevars name assum j') | RBinder(loc,BProd,name,c1,c2) -> @@ -364,7 +366,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let (mind,_) = try find_mrectype env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env - (nf_ise1 env !isevars cj.uj_val) (nf_ise1 env !isevars cj.uj_type) in + (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in let pj = match po with | Some p -> pretype mt_tycon env isevars p | None -> @@ -382,11 +384,11 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) try let expti = Indrec.branch_scheme env !isevars isrec i cj.uj_type in let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in - let efjt = nf_ise1 env !isevars fj.uj_type in + let efjt = nf_ise1 !isevars fj.uj_type in let pred = Indrec.pred_case_ml_onebranch env !isevars isrec (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in - if has_ise env !isevars pred then findtype (i+1) + if has_ise !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env !isevars pred in let k = Retyping.get_type_of env !isevars pty in @@ -394,8 +396,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) with UserError _ -> findtype (i+1) in findtype 1 in - let evalct = nf_ise1 env !isevars cj.uj_type - and evalPt = nf_ise1 env !isevars pj.uj_type in + let evalct = nf_ise1 !isevars cj.uj_type + and evalPt = nf_ise1 !isevars pj.uj_type in let (mind,bty,rsty) = Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in @@ -474,20 +476,20 @@ let j_apply f env sigma j = let ise_resolve fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon false isevars metamap env c in - j_apply (process_evars fail_evar) env !isevars j + j_apply (fun _ -> process_evars fail_evar) env !isevars j let ise_resolve_type fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine def_vty_con false isevars metamap env c in let tj = inh_ass_of_j env isevars j in - typed_app (strong (process_evars fail_evar) env !isevars) tj + typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj let ise_resolve_nocheck sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon true isevars metamap env c in - j_apply (process_evars true) env !isevars j + j_apply (fun _ -> process_evars true) env !isevars j let ise_resolve1 is_ass sigma env c = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b4fee1cd29..84097f8581 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -40,24 +40,25 @@ i*) (* Raw calls to the inference machine of Trad: boolean says if we must fail * on unresolved evars, or replace them by Metas *) -val ise_resolve : bool -> 'c evar_map -> (int * constr) list -> +val ise_resolve : bool -> unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment -val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list -> +val ise_resolve_type : bool -> unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> typed_type (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says * if we must coerce to a type *) -val ise_resolve1 : bool -> 'c evar_map -> unsafe_env -> rawconstr -> constr +val ise_resolve1 : bool -> unit evar_map -> unsafe_env -> rawconstr -> constr (* progmach.ml tries to type ill-typed terms: does not perform the conversion * test in application. *) -val ise_resolve_nocheck : 'c evar_map -> (int * constr) list -> +val ise_resolve_nocheck : unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment (* Internal of Trad... * Unused outside Trad, but useful for debugging *) -val pretype : bool * (constr option * constr option) - -> unsafe_env -> 'c evar_defs -> rawconstr -> unsafe_judgment +val pretype : + trad_constraint -> unsafe_env -> unit evar_defs -> rawconstr + -> unsafe_judgment diff --git a/proofs/typing_ev.ml b/pretyping/typing.ml index 741ef10409..c12f9bb34f 100644 --- a/proofs/typing_ev.ml +++ b/pretyping/typing.ml @@ -149,6 +149,7 @@ let execute_type env sigma constr = let j = execute { fix=false; nocheck=true } env sigma constr in assumption_of_judgment env sigma j -let execute_type env sigma constr = +let execute_rec_type env sigma constr = let j = execute { fix=false; nocheck=false } env sigma constr in assumption_of_judgment env sigma j + diff --git a/proofs/typing_ev.mli b/pretyping/typing.mli index b12cd369d3..b12cd369d3 100644 --- a/proofs/typing_ev.mli +++ b/pretyping/typing.mli diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4c14040bdd..80aae11823 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -33,7 +33,7 @@ type 'a clausenv = { type wc = walking_constraints let new_evar_in_sign env = - let hyps = get_globals (Environ.context env) in + let hyps = Environ.var_context env in let ev = new_evar () in DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))) @@ -881,10 +881,10 @@ let clenv_type_of ce c = | (n,Cltyp typ) -> (n,typ.rebus)) (intmap_to_list ce.env) in - failwith "TODO: clenv_type_of" + failwith "TODO" (*** - (Trad.ise_resolve true (w_Underlying ce.hook) metamap - (gLOB(w_hyps ce.hook)) c)._TYPE + (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap + (gLOB(w_hyps ce.hook)) c).uj_type ***) let clenv_instance_type_of ce c = diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index f3421cfdcc..e63648576d 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -10,7 +10,7 @@ open Term open Environ open Evd open Reduction -open Typing_ev +open Typing open Proof_trees open Logic open Refiner diff --git a/proofs/logic.ml b/proofs/logic.ml index b0823c1b2d..f89c6e9b4e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -10,7 +10,7 @@ open Term open Sign open Environ open Reduction -open Typing_ev +open Typing open Proof_trees open Typeops open Coqast @@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto = let prim_refiner r sigma goal = let env = goal.evar_env in - let sign = get_globals (context env) in + let sign = var_context env in let cl = goal.evar_concl in let info = goal.evar_info in match r with @@ -401,8 +401,8 @@ let prim_refiner r sigma goal = | _ -> anomaly "prim_refiner: Unrecognized primitive rule" let abst_value c = - let env = Global.env () in - Environ.abst_value (Typing.unsafe_env_of_env env) c + let env = Global.unsafe_env () in + Environ.abst_value env c let extract_constr = let rec crec vl = function diff --git a/proofs/logic.mli b/proofs/logic.mli index 2b2f9b8b44..88b632882e 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -15,8 +15,8 @@ open Proof_trees val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list val prim_extractor : - ((typed_type, constr) env -> proof_tree -> constr) -> - (typed_type, constr) env -> proof_tree -> constr + ((typed_type, constr) sign -> proof_tree -> constr) -> + (typed_type, constr) sign -> proof_tree -> constr val extract_constr : constr assumptions -> constr -> constr diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 3523f42182..ee0f3de895 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -8,7 +8,7 @@ open Sign open Evd open Stamps open Environ -open Typing_ev +open Typing type bindOcc = | Dep of identifier diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 834ee67343..1dc43f4134 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -714,7 +714,7 @@ let extract_pftreestate pts = [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ; 'sPC; 'sTR"Please ascend to the root" >]; let env = pts.tpf.goal.evar_env in - let hyps = get_globals (Environ.context env) in + let hyps = Environ.var_context env in strong whd_betadeltatiota env (ts_it pts.tpfsigma) (extract_proof hyps pts.tpf) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8bb6fba486..85f2973c03 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -11,7 +11,7 @@ open Instantiate open Environ open Reduction open Evd -open Typing_ev +open Typing open Tacred open Proof_trees open Logic @@ -45,7 +45,7 @@ let pf_concl gls = (sig_it gls).evar_concl let pf_untyped_hyps gls = let env = pf_env gls in - let (idl,tyl) = get_globals (Environ.context env) in + let (idl,tyl) = Environ.var_context env in (idl, List.map (fun x -> x.body) tyl) let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n @@ -69,6 +69,14 @@ let hnf_type_of gls = let pf_check_type gls c1 c2 = let casted = mkCast c1 c2 in pf_type_of gls casted +let pf_constr_of_com gls c = + let evc = project gls in + Astterm.constr_of_com evc (sig_it gls).hyps c + +let pf_constr_of_com_sort gls c = + let evc = project gls in + Astterm.constr_of_com_sort evc (sig_it gls).hyps c + let pf_reduction_of_redexp gls re c = reduction_of_redexp re (pf_env gls) (project gls) c @@ -242,7 +250,7 @@ let mutual_cofix lf lar pf = let rename_bound_var_goal gls = let { evar_env = env; evar_concl = cl } as gl = sig_it gls in - let ids = ids_of_sign (get_globals (Environ.context env)) in + let ids = ids_of_sign (Environ.var_context env) in convert_concl (rename_bound_var ids cl) gls diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 863023b79a..ea13c75a79 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,6 +41,9 @@ val pf_check_type : goal sigma -> constr -> constr -> constr val pf_fexecute : goal sigma -> constr -> unsafe_judgment val hnf_type_of : goal sigma -> constr -> constr +val pf_constr_of_com : goal sigma -> Coqast.t -> constr +val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr + val pf_get_hyp : goal sigma -> identifier -> constr val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr diff --git a/tactics/auto.ml b/tactics/auto.ml index 634e71f99a..2dc69c55bf 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,7 +10,7 @@ open Sign open Inductive open Evd open Reduction -open Typing_ev +open Typing open Tacmach open Proof_trees open Pfedit diff --git a/tactics/elim.ml b/tactics/elim.ml index 3fe9430c8c..2505f3b0a3 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -100,13 +100,13 @@ let dyn_decompose args gl = match args with | [Clause ids; Command c] -> decompose_these (pf_constr_of_com gl c) ids gl - | [CLAUSE ids; Constr c] -> + | [Clause ids; Constr c] -> decompose_these c ids gl | l -> bad_tactic_args "DecomposeThese" l gl let h_decompose = let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in - fun ids c -> v_decompose [(CLAUSE ids);(CONSTR c)] + fun ids c -> v_decompose [Clause ids; Constr c] let vernac_decompose_and = hide_constr_tactic "DecomposeAnd" decompose_and diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 04f96a8721..419488a37b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -273,17 +273,17 @@ let explain_refiner_cannot_applt k ctx t harg = P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1); P.pr_term k ctx harg >] -let error_occur_check ev rhs = +let explain_occur_check k ctx ev rhs = let id = "?" ^ string_of_int ev in - let pt = prterm rhs in + let pt = P.pr_term k ctx rhs in errorlabstrm "Trad.occur_check" [< 'sTR"Occur check failed: tried to define "; 'sTR id; 'sTR" with term"; 'bRK(1,1); pt >] -let error_not_clean sp t = - let c = Rel (List.hd (Listset.elements(free_rels t))) in +let explain_not_clean k ctx sp t = + let c = Rel (Intset.choose (free_rels t)) in let id = string_of_id (Names.basename sp) in - let var = pTERM(c) in + let var = P.pr_term k ctx c in errorlabstrm "Trad.not_clean" [< 'sTR"Tried to define "; 'sTR id; 'sTR" with a term using variable "; var; 'sPC; diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 7a16930698..02620168c1 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -10,7 +10,7 @@ open Sign open Constant open Inductive open Type_errors -open Typing +open Safe_typing open G_minicoq let (env : environment ref) = ref empty_environment |