aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-09-07 19:28:25 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-09-07 19:28:25 +0000
commitd331f7f1ac0ec2ed12d458597d558a1988db1ba6 (patch)
tree0e5addad213aeb1d647a0411285754e8a9cb23f6
parent11104cdcb1e53cd83768d2ce9858829b457e2d65 (diff)
deuxieme vague de modifs: evar_defs fonctionnel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend207
-rw-r--r--contrib/xml/proofTree2Xml.ml47
-rw-r--r--pretyping/cases.ml38
-rw-r--r--pretyping/cases.mli17
-rw-r--r--pretyping/clenv.ml18
-rw-r--r--pretyping/clenv.mli3
-rw-r--r--pretyping/coercion.ml95
-rw-r--r--pretyping/coercion.mli6
-rw-r--r--pretyping/evarconv.ml371
-rw-r--r--pretyping/evarconv.mli15
-rw-r--r--pretyping/evarutil.ml112
-rw-r--r--pretyping/evarutil.mli22
-rw-r--r--pretyping/pretyping.ml160
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/unification.ml100
-rw-r--r--pretyping/unification.mli5
-rw-r--r--proofs/clenvtac.ml37
-rw-r--r--proofs/clenvtac.mli13
-rw-r--r--proofs/evar_refiner.ml84
-rw-r--r--proofs/evar_refiner.mli22
-rw-r--r--proofs/refiner.ml9
-rw-r--r--proofs/refiner.mli2
-rw-r--r--tactics/eauto.ml47
-rw-r--r--tactics/equality.ml10
-rw-r--r--tactics/inv.ml3
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/setoid_replace.ml4
-rw-r--r--tactics/tacticals.ml7
-rw-r--r--tactics/tactics.ml67
29 files changed, 718 insertions, 732 deletions
diff --git a/.depend b/.depend
index e7f51f71b..c31f49e3d 100644
--- a/.depend
+++ b/.depend
@@ -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
@@ -153,9 +153,10 @@ pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \
pretyping/classops.cmi: library/decl_kinds.cmo kernel/environ.cmi \
pretyping/evd.cmi library/libnames.cmi library/libobject.cmi \
kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/term.cmi
-pretyping/clenv.cmi: pretyping/evd.cmi kernel/names.cmi lib/pp.cmi \
- pretyping/pretyping.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
- kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi
+pretyping/clenv.cmi: pretyping/evarutil.cmi pretyping/evd.cmi \
+ kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi pretyping/rawterm.cmi \
+ pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi \
+ pretyping/termops.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
@@ -323,11 +324,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
library/libnames.cmi kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -347,9 +348,9 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi
contrib/correctness/past.cmi: kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi lib/util.cmi
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi kernel/sign.cmi \
kernel/term.cmi
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
contrib/correctness/penv.cmi: library/libnames.cmi kernel/names.cmi \
@@ -477,6 +478,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx
ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi
ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi
+ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+ ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+ ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \
+ ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+ ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+ ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \
+ ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -499,14 +508,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi
ide/coq_tactics.cmo: ide/coq_tactics.cmi
ide/coq_tactics.cmx: ide/coq_tactics.cmi
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
- ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
- ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \
- ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
- ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
- ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \
- ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
@@ -659,6 +660,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/modops.cmi
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+ kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -667,12 +674,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi kernel/modops.cmi
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
- kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
lib/predicate.cmi lib/util.cmi kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -753,10 +754,10 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
@@ -765,24 +766,14 @@ lib/heap.cmo: lib/heap.cmi
lib/heap.cmx: lib/heap.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/pp_control.cmo: lib/pp_control.cmi
lib/pp_control.cmx: lib/pp_control.cmi
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/predicate.cmo: lib/predicate.cmi
lib/predicate.cmx: lib/predicate.cmi
lib/profile.cmo: lib/profile.cmi
lib/profile.cmx: lib/profile.cmi
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/compat.cmo lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi
library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -889,6 +880,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
lib/system.cmx library/states.cmi
library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi
library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/compat.cmo lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi
parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
toplevel/vernacexpr.cmo
@@ -1276,13 +1277,15 @@ pretyping/clenv.cmx: pretyping/coercion.cmx kernel/environ.cmx \
pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
pretyping/evarconv.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
kernel/names.cmi pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
- pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
- kernel/term.cmi kernel/typeops.cmi lib/util.cmi pretyping/coercion.cmi
+ pretyping/recordops.cmi kernel/reduction.cmi pretyping/reductionops.cmi \
+ pretyping/retyping.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+ pretyping/coercion.cmi
pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
pretyping/evarconv.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
kernel/names.cmx pretyping/pretype_errors.cmx pretyping/rawterm.cmx \
- pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
- kernel/term.cmx kernel/typeops.cmx lib/util.cmx pretyping/coercion.cmi
+ pretyping/recordops.cmx kernel/reduction.cmx pretyping/reductionops.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 \
@@ -1298,13 +1301,13 @@ pretyping/detyping.cmx: kernel/declarations.cmx kernel/environ.cmx \
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 pretyping/reductionops.cmi kernel/term.cmi \
- pretyping/typing.cmi lib/util.cmi pretyping/evarconv.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 pretyping/reductionops.cmx kernel/term.cmx \
- pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi
+ 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 \
@@ -1466,13 +1469,15 @@ pretyping/unification.cmo: kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/pattern.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 \
- pretyping/typing.cmi lib/util.cmi pretyping/unification.cmi
+ kernel/type_errors.cmi pretyping/typing.cmi lib/util.cmi \
+ pretyping/unification.cmi
pretyping/unification.cmx: kernel/environ.cmx pretyping/evarutil.cmx \
pretyping/evd.cmx library/global.cmx library/nameops.cmx kernel/names.cmx \
pretyping/pattern.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 \
- pretyping/typing.cmx lib/util.cmx pretyping/unification.cmi
+ kernel/type_errors.cmx pretyping/typing.cmx lib/util.cmx \
+ pretyping/unification.cmi
proofs/clenvtac.cmo: pretyping/clenv.cmi kernel/environ.cmi \
proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
@@ -1490,22 +1495,20 @@ proofs/clenvtac.cmx: pretyping/clenv.cmx kernel/environ.cmx \
kernel/term.cmx pretyping/termops.cmx pretyping/unification.cmx \
lib/util.cmx proofs/clenvtac.cmi
proofs/evar_refiner.cmo: interp/constrintern.cmi kernel/environ.cmi \
- pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
- proofs/logic.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \
- lib/pp.cmi pretyping/pretyping.cmi proofs/proof_trees.cmi \
- proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \
- proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo \
- pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \
- kernel/type_errors.cmi pretyping/typing.cmi lib/util.cmi \
+ pretyping/evarutil.cmi pretyping/evd.cmi proofs/logic.cmi \
+ library/nameops.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+ pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \
+ proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \
+ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \
proofs/evar_refiner.cmi
proofs/evar_refiner.cmx: interp/constrintern.cmx kernel/environ.cmx \
- pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
- proofs/logic.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \
- lib/pp.cmx pretyping/pretyping.cmx proofs/proof_trees.cmx \
- proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \
- proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \
- pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \
- kernel/type_errors.cmx pretyping/typing.cmx lib/util.cmx \
+ pretyping/evarutil.cmx pretyping/evd.cmx proofs/logic.cmx \
+ library/nameops.cmx kernel/names.cmx lib/pp.cmx pretyping/pretyping.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
+ proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \
+ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \
proofs/evar_refiner.cmi
proofs/logic.cmo: interp/constrextern.cmi kernel/environ.cmi \
pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
@@ -2225,20 +2228,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi
toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi
-toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
- parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
- kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
- lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
- library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
- proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
- toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
- parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
- kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
- lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
- library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
- proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
- toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2303,6 +2292,20 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+ parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+ lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
+ library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
+ proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
+ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+ parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+ lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
+ library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
+ proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
+ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi library/lib.cmi \
@@ -2389,6 +2392,12 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \
tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
+ contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
+ contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2403,12 +2412,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
toplevel/record.cmx kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
- kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
- contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
- kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
- contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: interp/constrintern.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi kernel/term.cmi \
pretyping/termops.cmi contrib/correctness/pdb.cmi
@@ -2983,6 +2986,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \
pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/showproof.cmo: pretyping/clenv.cmi interp/constrintern.cmi \
parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -3007,14 +3018,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 \
@@ -3197,12 +3200,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 \
@@ -3249,20 +3252,18 @@ contrib/xml/proofTree2Xml.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
contrib/xml/cic2acic.cmo kernel/environ.cmi pretyping/evd.cmi \
library/global.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \
lib/pp.cmi parsing/pptactic.cmi translate/pptacticnew.cmi \
- parsing/printer.cmi contrib/xml/proof2aproof.cmo proofs/proof_trees.cmi \
- proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi \
+ parsing/printer.cmi contrib/xml/proof2aproof.cmo proofs/proof_type.cmi \
+ kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi \
contrib/xml/unshare.cmi lib/util.cmi contrib/xml/xml.cmi
contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
contrib/xml/cic2acic.cmx kernel/environ.cmx pretyping/evd.cmx \
library/global.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \
lib/pp.cmx parsing/pptactic.cmx translate/pptacticnew.cmx \
- parsing/printer.cmx contrib/xml/proof2aproof.cmx proofs/proof_trees.cmx \
- proofs/proof_type.cmx kernel/sign.cmx proofs/tacexpr.cmx kernel/term.cmx \
+ parsing/printer.cmx contrib/xml/proof2aproof.cmx proofs/proof_type.cmx \
+ kernel/sign.cmx proofs/tacexpr.cmx kernel/term.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 \
@@ -3291,10 +3292,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
- ide/utils/configwin_types.cmo ide/utils/configwin.cmi
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
- ide/utils/configwin_types.cmx ide/utils/configwin.cmi
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
ide/utils/uoptions.cmi
@@ -3305,6 +3304,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi
ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+ ide/utils/configwin_types.cmo ide/utils/configwin.cmi
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+ ide/utils/configwin_types.cmx ide/utils/configwin.cmi
ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
ide/utils/uoptions.cmi
ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index b9b66774a..423991784 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -95,7 +95,7 @@ let string_of_prim_rule x = match x with
let
- print_proof_tree curi sigma0 pf proof_tree_to_constr
+ print_proof_tree curi sigma pf proof_tree_to_constr
proof_tree_to_flattened_proof_tree constr_to_ids
=
let module PT = Proof_type in
@@ -164,10 +164,7 @@ Pp.ppnl (Pp.(++) (Pp.str
let {Evd.evar_concl=concl;
Evd.evar_hyps=hyps}=goal in
- let rc = (Proof_trees.rc_of_gc sigma0 goal) in
- let sigma = Proof_trees.get_gc rc in
- let hyps = Proof_trees.get_hyps rc in
- let env= Proof_trees.get_env rc in
+ let env = Global.env_of_context hyps in
let xgoal =
X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7be919320..463788a22 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,7 +63,8 @@ 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 = new_isevar isevars env loc (new_Type ())
+let mkExistential isevars env loc =
+ e_new_isevar isevars env loc (new_Type ())
let norec_branch_scheme env isevars cstr =
let rec crec env = function
@@ -378,7 +379,7 @@ let push_history_pattern n current cont =
*)
type pattern_matching_problem =
{ env : env;
- isevars : evar_defs;
+ isevars : evar_defs ref;
pred : predicate_signature option;
tomatch : tomatch_stack;
history : pattern_continuation;
@@ -404,7 +405,7 @@ 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 (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
@@ -412,12 +413,12 @@ let inh_coerce_to_ind isevars env tmloc ty tyi =
List.fold_right
(fun (na,ty) (env,evl,n) ->
(push_rel (na,None,ty) env,
- (new_isevar isevars env (hole_source n) ty)::evl,n+1))
+ (e_new_isevar isevars env (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
un inductif cela doit être égal *)
- if the_conv_x_leq env isevars expected_typ ty then ty
+ if e_cumul env isevars expected_typ ty then ty
else raise NotCoercible
(* We do the unification for all the rows that contain
@@ -431,17 +432,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 (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 (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 (evars_of !isevars) typ)
with Not_found -> NotInd (None,typ)
let coerce_row typing_fun isevars env cstropt tomatch =
@@ -929,7 +930,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 (evars_of !isevars))) typs
in
let eqns = array_map2 prepare_unif_pb typs cstrs in
(* First strategy: no dependencies at all *)
@@ -942,7 +943,7 @@ let infer_predicate loc env isevars typs cstrs indf =
else
mkExistential isevars env (loc, CasesType)
in
- if array_for_all (fun (_,_,typ) -> the_conv_x_leq env isevars typ mtyp) eqns
+ if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
then
(* Non dependent case -> turn it into a (dummy) dependent one *)
let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
@@ -1127,7 +1128,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 (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
@@ -1367,7 +1368,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 (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 *)
@@ -1585,7 +1586,7 @@ 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 (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 *)
@@ -1699,21 +1700,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 = 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 _)) ->
- evars_reset_evd isevars_copy isevars;
+ isevars := 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 _)) ->
- evars_reset_evd isevars_copy isevars;
+ isevars := 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 *)
@@ -1769,5 +1770,8 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
List.iter (check_unused_pattern env) matx;
match tycon with
- | Some p -> Coercion.inh_conv_coerce_to loc env isevars j p
+ | Some p ->
+ let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+ isevars := evd';
+ j
| None -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 54fdc2c09..de63ea525 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -34,7 +34,7 @@ exception PatternMatchingError of env * pattern_matching_error
(*s Used for old cases in pretyping *)
val branch_scheme :
- env -> evar_defs -> bool -> inductive_family -> constr array
+ env -> evar_defs ref -> bool -> inductive_family -> constr array
type ml_case_error =
| MlCaseAbsurd
@@ -48,9 +48,12 @@ val pred_case_ml : (* raises [NotInferable] if not inferable *)
(*s Compilation of pattern-matching. *)
val compile_cases :
- loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
- * evar_defs -> type_constraint -> env ->
- (rawconstr option * rawconstr option ref) *
- (rawconstr * (name * (loc * inductive * name list) option) ref) list *
- (loc * identifier list * cases_pattern list * rawconstr) list ->
- unsafe_judgment
+ loc ->
+ (type_constraint -> env -> rawconstr -> unsafe_judgment) *
+ evar_defs ref ->
+ type_constraint ->
+ env ->
+ (rawconstr option * rawconstr option ref) *
+ (rawconstr * (name * (loc * inductive * name list) option) ref) list *
+ (loc * identifier list * cases_pattern list * rawconstr) list ->
+ unsafe_judgment
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 0df34169a..7753ec7ed 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -23,6 +23,7 @@ open Pattern
open Tacexpr
open Tacred
open Pretype_errors
+open Evarutil
(* *)
let get_env evc = Global.env_of_context evc.it
@@ -157,8 +158,9 @@ let connect_clenv gls clenv =
{ clenv with hook = wc }
let clenv_wtactic f clenv =
- let (sigma',mmap') = f (clenv.hook.sigma, clenv.env) in
- {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=sigma'}}
+ let (evd',mmap') =
+ f (create_evar_defs clenv.hook.sigma, clenv.env) in
+ {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
let mk_clenv_hnf_constr_type_of wc t =
mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
@@ -411,10 +413,9 @@ let clenv_independent clenv =
let w_coerce wc c ctyp target =
let j = make_judge c ctyp in
let env = get_env wc in
- let isevars = Evarutil.create_evar_defs wc.sigma in
- let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
- (* faire quelque chose avec isevars ? *)
- j'.uj_val
+ let isevars = create_evar_defs wc.sigma in
+ let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
+ (evars_of evd',j'.uj_val)
let clenv_constrain_dep_args hyps_only clause = function
| [] -> clause
@@ -427,7 +428,8 @@ let clenv_constrain_dep_args hyps_only clause = function
try
let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in
let c_typ = w_hnf_constr wc (w_type_of wc c) in
- let c' = w_coerce wc c c_typ k_typ in
+ (* faire quelque chose avec le sigma retourne ? *)
+ let (_,c') = w_coerce wc c c_typ k_typ in
clenv_unify true CONV (mkMeta k) c' clenv
with _ ->
clenv_unify true CONV (mkMeta k) c clenv)
@@ -485,7 +487,7 @@ let clenv_match_args s clause =
with _ ->
(* Try to coerce to the type of [k]; cannot merge with the
previous case because Coercion does not handle Meta *)
- let c' = w_coerce clause.hook c c_typ k_typ in
+ let (_,c') = w_coerce clause.hook c c_typ k_typ in
try clenv_unify true CONV (mkMeta k) c' clause
with PretypeError (env,CannotUnify (m,n)) ->
Stdpp.raise_with_loc loc
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index ae5cafdf6..d3f36e720 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -14,6 +14,7 @@ open Names
open Term
open Sign
open Evd
+open Evarutil
(*i*)
(* [new_meta] is a generator of unique meta variables *)
@@ -56,7 +57,7 @@ val mk_clenv_type_of : wc -> constr -> wc clausenv
val subst_clenv : (substitution -> 'a -> 'a) ->
substitution -> 'a clausenv -> 'a clausenv
val clenv_wtactic :
- (evar_map * meta_map -> evar_map * meta_map) -> wc clausenv -> wc clausenv
+ (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ddbdf94b4..347bc7b8e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -77,16 +77,16 @@ let apply_coercion env p hj typ_cl =
let inh_app_fun env isevars j =
let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
match kind_of_term t with
- | Prod (_,_,_) -> j
+ | Prod (_,_,_) -> (isevars,j)
| Evar ev when not (is_defined_evar isevars ev) ->
- let t = define_evar_as_arrow isevars ev in
- { uj_val = j.uj_val; uj_type = t }
+ let (isevars',t) = define_evar_as_arrow isevars ev in
+ (isevars',{ uj_val = j.uj_val; uj_type = t })
| _ ->
(try
let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
let p = lookup_path_to_fun_from i1 in
- apply_coercion env p j t
- with Not_found -> j)
+ (isevars,apply_coercion env p j t)
+ with Not_found -> (isevars,j))
let inh_tosort_force env isevars j =
try
@@ -99,13 +99,13 @@ let inh_tosort_force env isevars j =
let inh_coerce_to_sort env isevars j =
let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
match kind_of_term typ with
- | Sort s -> { utj_val = j.uj_val; utj_type = s }
+ | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined_evar isevars ev) ->
- let s = define_evar_as_sort isevars ev in
- { utj_val = j.uj_val; utj_type = s }
+ let (isevars',s) = define_evar_as_sort isevars ev in
+ (isevars',{ utj_val = j.uj_val; utj_type = s })
| _ ->
let j1 = inh_tosort_force env isevars j in
- type_judgment env (j_nf_evar (evars_of isevars) j1)
+ (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
let inh_coerce_to_fail env isevars c1 hj =
let hj' =
@@ -116,33 +116,34 @@ let inh_coerce_to_fail env isevars c1 hj =
apply_coercion env p hj t2
with Not_found -> raise NoCoercion
in
- if the_conv_x_leq env isevars hj'.uj_type c1 then
- hj'
- else
- raise NoCoercion
+ try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+ with Reduction.NotConvertible -> raise NoCoercion
let rec inh_conv_coerce_to_fail env isevars hj c1 =
let {uj_val = v; uj_type = t} = hj in
- if the_conv_x_leq env isevars t c1 then hj
- else
- try
+ try (the_conv_x_leq env t c1 isevars, hj)
+ with Reduction.NotConvertible ->
+ (try
inh_coerce_to_fail env isevars c1 hj
- with NoCoercion -> (* try ... with _ -> ... is BAD *)
+ with NoCoercion ->
(match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
| Prod (_,t1,t2), Prod (name,u1,u2) ->
let v' = whd_betadeltaiota env (evars_of isevars) v in
- if (match kind_of_term v' with
- | Lambda (_,v1,v2) ->
- the_conv_x env isevars v1 u1 (* leq v1 u1? *)
- | _ -> false)
+ let (evd',b) =
+ match kind_of_term v' with
+ | Lambda (_,v1,v2) ->
+ (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *)
+ with Reduction.NotConvertible -> (isevars, false))
+ | _ -> (isevars,false) in
+ if b
then
let (x,v1,v2) = destLambda v' in
let env1 = push_rel (x,None,v1) env in
- let h2 = inh_conv_coerce_to_fail env1 isevars
+ let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
{uj_val = v2; uj_type = t2 } u2 in
- { uj_val = mkLambda (x, v1, h2.uj_val);
- uj_type = mkProd (x, v1, h2.uj_type) }
+ (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
+ uj_type = mkProd (x, v1, h2.uj_type) })
else
(* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
(* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
@@ -151,57 +152,27 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 =
| Anonymous -> Name (id_of_string "x")
| _ -> name) in
let env1 = push_rel (name,None,u1) env in
- let h1 =
+ let (evd',h1) =
inh_conv_coerce_to_fail env1 isevars
{uj_val = mkRel 1; uj_type = (lift 1 u1) }
(lift 1 t1) in
- let h2 = inh_conv_coerce_to_fail env1 isevars
+ let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
{ uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
uj_type = subst1 h1.uj_val t2 }
u2
in
- { uj_val = mkLambda (name, u1, h2.uj_val);
- uj_type = mkProd (name, u1, h2.uj_type) }
- | _ -> raise NoCoercion)
+ (evd'',
+ { uj_val = mkLambda (name, u1, h2.uj_val);
+ uj_type = mkProd (name, u1, h2.uj_type) })
+ | _ -> raise NoCoercion))
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj t =
- let cj' =
+ let (evd',cj') =
try
inh_conv_coerce_to_fail env isevars cj t
with NoCoercion ->
let sigma = evars_of isevars in
error_actual_type_loc loc env sigma cj t
in
- { uj_val = cj'.uj_val; uj_type = t }
-
-(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
- args)] of type [tycon] (if any) by inserting coercions in front of
- each arg$_i$, if necessary *)
-
-let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
- let rec apply_rec env n resj = function
- | [] -> resj
- | (loc,hj)::restjl ->
- let sigma = evars_of isevars in
- let resj = inh_app_fun env isevars resj in
- let ntyp = whd_betadeltaiota env sigma resj.uj_type in
- match kind_of_term ntyp with
- | Prod (na,c1,c2) ->
- let hj' =
- try
- inh_conv_coerce_to_fail env isevars hj c1
- with NoCoercion ->
- error_cant_apply_bad_type_loc apploc env sigma
- (1,c1,hj.uj_type) resj (List.map snd restjl) in
- let newresj =
- { uj_val = applist (j_val resj, [j_val hj']);
- uj_type = subst1 hj'.uj_val c2 } in
- apply_rec (push_rel (na,None,c1) env) (n+1) newresj restjl
- | _ ->
- error_cant_apply_not_functional_loc
- (join_loc funloc loc) env sigma resj
- (List.map snd restjl)
- in
- apply_rec env 1 funj argjl
-
+ (evd',{ uj_val = cj'.uj_val; uj_type = t })
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cf24829c1..85b4c7506 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -25,19 +25,19 @@ open Rawterm
inserts a coercion into [j], if needed, in such a way it gets as
type a product; it returns [j] if no coercion is applicable *)
val inh_app_fun :
- env -> evar_defs -> unsafe_judgment -> unsafe_judgment
+ env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
(* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type a sort; it fails if no coercion is applicable *)
val inh_coerce_to_sort :
- env -> evar_defs -> unsafe_judgment -> unsafe_type_judgment
+ env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
(* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
- env -> evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
+ env -> evar_defs -> unsafe_judgment -> constr -> evar_defs * unsafe_judgment
(* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3ca777647..6454e0e84 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -125,6 +125,44 @@ let check_conv_record (t1,l1) (t2,l2) =
(* Precondition: one of the terms of the pb is an uninstanciated evar,
* possibly applied to arguments. *)
+let rec ise_try isevars = function
+ [] -> assert false
+ | [f] -> f isevars
+ | f1::l ->
+ let (isevars',b) = f1 isevars in
+ if b then (isevars',b) else ise_try isevars l
+
+let ise_and isevars l =
+ let rec ise_and i = function
+ [] -> assert false
+ | [f] -> f i
+ | f1::l ->
+ let (i',b) = f1 i in
+ if b then ise_and i' l else (isevars,false) in
+ ise_and isevars l
+
+let ise_list2 isevars f l1 l2 =
+ let rec ise_list2 i l1 l2 =
+ match l1,l2 with
+ [], [] -> (i, true)
+ | [x], [y] -> f i x y
+ | x::l1, y::l2 ->
+ let (i',b) = f i x y in
+ if b then ise_list2 i' l1 l2 else (isevars,false)
+ | _ -> (isevars, false) in
+ ise_list2 isevars l1 l2
+
+let ise_array2 isevars f v1 v2 =
+ let rec allrec i = function
+ | -1 -> (i,true)
+ | n ->
+ let (i',b) = f i v1.(n) v2.(n) in
+ if b then allrec i' (n-1) else (isevars,false)
+ in
+ let lv1 = Array.length v1 in
+ if lv1 = Array.length v2 then allrec isevars (pred lv1)
+ else (isevars,false)
+
let rec evar_conv_x env isevars pbty term1 term2 =
let sigma = evars_of isevars in
let term1 = whd_castappevar sigma term1 in
@@ -136,11 +174,12 @@ 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 *)
- (not (has_undefined_isevars isevars term1) &
- not (has_undefined_isevars isevars term2) &
- is_fconv pbty env (evars_of isevars) term1 term2)
- or
- if ise_undefined isevars term1 then
+ if
+ (not (has_undefined_isevars isevars term1) &
+ not (has_undefined_isevars isevars term2) &
+ is_fconv pbty env (evars_of isevars) term1 term2) then
+ (isevars,true)
+ else if ise_undefined isevars term1 then
solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
else if ise_undefined isevars term2 then
solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1)
@@ -150,7 +189,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
then
- (add_conv_pb isevars (pbty,applist(t1,l1),applist(t2,l2)); true)
+ (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
else
evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
@@ -158,67 +197,81 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Evar must be undefined since we have whd_ised *)
match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
- let f1 () =
+ let f1 i =
if List.length l1 > List.length l2 then
let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
- solve_simple_eqn evar_conv_x env isevars
- (pbty,ev2,applist(term1,deb1))
- & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+ ise_and i
+ [(fun i -> solve_simple_eqn evar_conv_x env i
+ (pbty,ev2,applist(term1,deb1)));
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) rest1 l2)]
else
let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
- solve_simple_eqn evar_conv_x env isevars
- (pbty,ev1,applist(term2,deb2))
- & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
- and f2 () =
- (sp1 = sp2)
- & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)
- & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+ ise_and i
+ [(fun i -> solve_simple_eqn evar_conv_x env i
+ (pbty,ev1,applist(term2,deb2)));
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 rest2)]
+ and f2 i =
+ if sp1 = sp2 then
+ ise_and i
+ [(fun i -> ise_array2 i
+ (fun i -> evar_conv_x env i CONV) al1 al2);
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 l2)]
+ else (i,false)
in
ise_try isevars [f1; f2]
| Flexible ev1, MaybeFlexible flex2 ->
- let f1 () =
- (List.length l1 <= List.length l2) &
- let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
- (* First compare extra args for better failure message *)
- list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 &
- evar_conv_x env isevars pbty term1 (applist(term2,deb2))
- and f4 () =
+ let f1 i =
+ if List.length l1 <= List.length l2 then
+ let (deb2,rest2) =
+ list_chop (List.length l2-List.length l1) l2 in
+ ise_and i
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 rest2);
+ (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
+ else (i,false)
+ and f4 i =
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env isevars pbty
- appr1 (evar_apprec env isevars l2 v2)
- | None -> false
+ evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ | None -> (i,false)
in
ise_try isevars [f1; f4]
| MaybeFlexible flex1, Flexible ev2 ->
- let f1 () =
- (List.length l2 <= List.length l1) &
- let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
- (* First compare extra args for better failure message *)
- list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 &
- evar_conv_x env isevars pbty (applist(term1,deb1)) term2
- and f4 () =
+ let f1 i =
+ if List.length l2 <= List.length l1 then
+ let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+ ise_and i
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) rest1 l2);
+ (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
+ else (i,false)
+ and f4 i =
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env isevars pbty
- (evar_apprec env isevars l1 v1) appr2
- | None -> false
+ evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ | None -> (i,false)
in
ise_try isevars [f1; f4]
| MaybeFlexible flex1, MaybeFlexible flex2 ->
- let f2 () =
- (flex1 = flex2)
- & (List.length l1 = List.length l2)
- & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
- and f3 () =
- (try conv_record env isevars
+ let f2 i =
+ if flex1 = flex2 then
+ ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+ else (i,false)
+ and f3 i =
+ (try conv_record env i
(try check_conv_record appr1 appr2
with Not_found -> check_conv_record appr2 appr1)
- with _ -> false)
- and f4 () =
+(* TODO: remove this _ !!! *)
+ with _ -> (i,false))
+ and f4 i =
(* heuristic: unfold second argument first, exception made
if the first argument is a beta-redex (expand a constant
only if necessary) *)
@@ -228,57 +281,55 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| _ -> eval_flexible_term env flex2 in
match val2 with
| Some v2 ->
- evar_eqappr_x env isevars pbty
- appr1 (evar_apprec env isevars l2 v2)
+ evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
| None ->
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env isevars pbty
- (evar_apprec env isevars l1 v1) appr2
- | None -> false
+ evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ | None -> (i,false)
in
ise_try isevars [f2; f3; f4]
| Flexible ev1, Rigid _ ->
- (List.length l1 <= List.length l2) &
- let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
- (* First compare extra args for better failure message *)
- list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 &
- solve_simple_eqn evar_conv_x env isevars
- (pbty,ev1,applist(term2,deb2))
-
+ if (List.length l1 <= List.length l2) then
+ let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+ ise_and isevars
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
+ (fun i -> solve_simple_eqn evar_conv_x env i
+ (pbty,ev1,applist(term2,deb2)))]
+ else (isevars,false)
| Rigid _, Flexible ev2 ->
- (List.length l2 <= List.length l1) &
- let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
- (* First compare extra args for better failure message *)
- list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 &
- solve_simple_eqn evar_conv_x env isevars
- (pbty,ev2,applist(term1,deb1))
-
+ if List.length l2 <= List.length l1 then
+ let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+ ise_and isevars
+ (* First compare extra args for better failure message *)
+ [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
+ (fun i -> solve_simple_eqn evar_conv_x env i
+ (pbty,ev2,applist(term1,deb1)))]
+ else (isevars,false)
| MaybeFlexible flex1, Rigid _ ->
- let f3 () =
- (try conv_record env isevars (check_conv_record appr1 appr2)
- with _ -> false)
- and f4 () =
+ let f3 i =
+ (try conv_record env i (check_conv_record appr1 appr2)
+ with _ -> (i,false))
+ and f4 i =
match eval_flexible_term env flex1 with
| Some v1 ->
- evar_eqappr_x env isevars pbty
- (evar_apprec env isevars l1 v1) appr2
- | None -> false
+ evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ | None -> (i,false)
in
ise_try isevars [f3; f4]
| Rigid _ , MaybeFlexible flex2 ->
- let f3 () =
- (try (conv_record env isevars (check_conv_record appr2 appr1))
- with _ -> false)
- and f4 () =
+ let f3 i =
+ (try (conv_record env i (check_conv_record appr2 appr1))
+ with _ -> (i,false))
+ and f4 i =
match eval_flexible_term env flex2 with
| Some v2 ->
- evar_eqappr_x env isevars pbty
- appr1 (evar_apprec env isevars l2 v2)
- | None -> false
+ evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ | None -> (i,false)
in
ise_try isevars [f3; f4]
@@ -288,27 +339,30 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| _, Cast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2)
- | Sort s1, Sort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2
+ | Sort s1, Sort s2 when l1=[] & l2=[] ->
+ (isevars,base_sort_cmp pbty s1 s2)
| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] ->
- evar_conv_x env isevars CONV c1 c2
- &
- (let c = nf_evar (evars_of isevars) c1 in
- evar_conv_x (push_rel (na,None,c) env) isevars CONV c'1 c'2)
+ ise_and isevars
+ [(fun i -> evar_conv_x env i CONV c1 c2);
+ (fun i ->
+ let c = nf_evar (evars_of i) c1 in
+ evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
- let f1 () =
- evar_conv_x env isevars CONV b1 b2
- &
- (let b = nf_evar (evars_of isevars) b1 in
- let t = nf_evar (evars_of isevars) t1 in
- evar_conv_x (push_rel (na,Some b,t) env) isevars pbty c'1 c'2)
- & (List.length l1 = List.length l2)
- & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
- and f2 () =
- let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1)
- and appr2 = evar_apprec env isevars l2 (subst1 b2 c'2)
- in evar_eqappr_x env isevars pbty appr1 appr2
+ let f1 i =
+ ise_and i
+ [(fun i -> evar_conv_x env i CONV b1 b2);
+ (fun i ->
+ let b = nf_evar (evars_of i) b1 in
+ let t = nf_evar (evars_of i) t1 in
+ evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 l2)]
+ and f2 i =
+ let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
+ and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
+ in evar_eqappr_x env i pbty appr1 appr2
in
ise_try isevars [f1; f2]
@@ -321,71 +375,102 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
in evar_eqappr_x env isevars pbty appr1 appr2
| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
- evar_conv_x env isevars CONV c1 c2
- &
- (let c = nf_evar (evars_of isevars) c1 in
- evar_conv_x (push_rel (n,None,c) env) isevars pbty c'1 c'2)
+ ise_and isevars
+ [(fun i -> evar_conv_x env i CONV c1 c2);
+ (fun i ->
+ let c = nf_evar (evars_of i) c1 in
+ evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
| Ind sp1, Ind sp2 ->
- sp1=sp2
- & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
-
+ if sp1=sp2 then
+ ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
+ else (isevars, false)
+
| Construct sp1, Construct sp2 ->
- sp1=sp2
- & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+ if sp1=sp2 then
+ ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2
+ else (isevars, false)
| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
- evar_conv_x env isevars CONV p1 p2
- & evar_conv_x env isevars CONV c1 c2
- & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
- & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+ ise_and isevars
+ [(fun i -> evar_conv_x env i CONV p1 p2);
+ (fun i -> evar_conv_x env i CONV c1 c2);
+ (fun i -> ise_array2 i
+ (fun i -> evar_conv_x env i CONV) cl1 cl2);
+ (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)]
| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
- li1=li2
- & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
- & (array_for_all2
- (evar_conv_x (push_rec_types recdef1 env) isevars CONV)
- bds1 bds2)
- & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-
+ if li1=li2 then
+ ise_and isevars
+ [(fun i -> ise_array2 i
+ (fun i -> evar_conv_x env i CONV) tys1 tys2);
+ (fun i -> ise_array2 i
+ (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+ bds1 bds2);
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 l2)]
+ else (isevars,false)
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
- i1=i2
- & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2)
- & (array_for_all2
- (evar_conv_x (push_rec_types recdef1 env) isevars CONV)
- bds1 bds2)
- & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
-
- | (Meta _ | Lambda _), _ -> false
- | _, (Meta _ | Lambda _) -> false
-
- | (Ind _ | Construct _ | Sort _ | Prod _), _ -> false
- | _, (Ind _ | Construct _ | Sort _ | Prod _) -> false
+ if i1=i2 then
+ ise_and isevars
+ [(fun i -> ise_array2 i
+ (fun i -> evar_conv_x env i CONV) tys1 tys2);
+ (fun i -> ise_array2 i
+ (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+ bds1 bds2);
+ (fun i -> ise_list2 i
+ (fun i -> evar_conv_x env i CONV) l1 l2)]
+ else (isevars,false)
+
+ | (Meta _ | Lambda _), _ -> (isevars,false)
+ | _, (Meta _ | Lambda _) -> (isevars,false)
+
+ | (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false)
+ | _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false)
| (App _ | Case _ | Fix _ | CoFix _),
- (App _ | Case _ | Fix _ | CoFix _) -> false
+ (App _ | Case _ | Fix _ | CoFix _) -> (isevars,false)
| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
- let ks =
+ let (isevars',ks) =
List.fold_left
- (fun ks b ->
+ (fun (i,ks) b ->
let dloc = (dummy_loc,Rawterm.InternalHole) in
- (new_isevar isevars env dloc (substl ks b)) :: ks)
- [] bs
+ let (i',ev) = new_isevar i env dloc (substl ks b) in
+ (i', ev :: ks))
+ (isevars,[]) bs
in
- (list_for_all2eq
- (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
- us2 us)
- &
- (list_for_all2eq
- (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
- params1 params)
- & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
- & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
+ ise_and isevars'
+ [(fun i ->
+ ise_list2 i
+ (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+ us2 us);
+ (fun i ->
+ ise_list2 i
+ (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
+ params1 params);
+ (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
+ (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
-let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2
-let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
+let the_conv_x env t1 t2 isevars =
+ match evar_conv_x env isevars CONV t1 t2 with
+ (evd',true) -> evd'
+ | _ -> raise Reduction.NotConvertible
+
+let the_conv_x_leq env t1 t2 isevars =
+ match evar_conv_x env isevars CUMUL t1 t2 with
+ (evd', true) -> evd'
+ | _ -> raise Reduction.NotConvertible
+let e_conv env isevars t1 t2 =
+ match evar_conv_x env !isevars CONV t1 t2 with
+ (evd',true) -> isevars := evd'; true
+ | _ -> false
+
+let e_cumul env isevars t1 t2 =
+ match evar_conv_x env !isevars CUMUL t1 t2 with
+ (evd',true) -> isevars := evd'; true
+ | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index c8b234ee2..5deccaa8b 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,13 +16,20 @@ open Reductionops
open Evarutil
(*i*)
-val the_conv_x : env -> evar_defs -> constr -> constr -> bool
+(* returns exception Reduction.NotConvertible if not unifiable *)
+val the_conv_x : env -> constr -> constr -> evar_defs -> evar_defs
+val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
-val the_conv_x_leq : env -> evar_defs -> constr -> constr -> bool
+(* The same function resolving evars by side-effect and
+ catching the exception *)
+val e_conv : env -> evar_defs ref -> constr -> constr -> bool
+val e_cumul : env -> evar_defs ref -> constr -> constr -> bool
(*i For debugging *)
-val evar_conv_x : env -> evar_defs -> conv_pb -> constr -> constr -> bool
+val evar_conv_x :
+ env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool
val evar_eqappr_x :
env -> evar_defs ->
- conv_pb -> constr * constr list -> constr * constr list -> bool
+ conv_pb -> constr * constr list -> constr * constr list ->
+ evar_defs * bool
(*i*)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f5b8c6288..aa079e7ce 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -218,32 +218,18 @@ let do_restrict_hyps sigma ev args =
type evar_constraint = conv_pb * constr * constr
type evar_defs =
- { mutable evars : Evd.evar_map;
- mutable conv_pbs : evar_constraint list;
- mutable history : (existential_key * (loc * Rawterm.hole_kind)) list }
+ { evars : Evd.evar_map;
+ conv_pbs : evar_constraint list;
+ history : (existential_key * (loc * Rawterm.hole_kind)) list }
let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
let evars_of d = d.evars
-let evars_reset_evd evd d = d.evars <- evd
-let add_conv_pb d pb = d.conv_pbs <- pb::d.conv_pbs
+let evars_reset_evd evd d = {d with evars = evd}
+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)
-(* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
- * when fi returns false or an exception. Returns true if one of the fi
- * returns true, and false if every fi return false (in the latter case,
- * the evar constraints are restored).
- *)
-let ise_try isevars l =
- let u = isevars.evars in
- let rec test = function
- [] -> isevars.evars <- u; false
- | f::l ->
- (try f() with reraise -> isevars.evars <- u; raise reraise)
- or (isevars.evars <- u; test l)
- in test l
-
(* say if the section path sp corresponds to an existential *)
let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp
@@ -253,7 +239,7 @@ 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.evars <- Evd.define isevars.evars sp body
+ {isevars with evars = Evd.define isevars.evars sp body}
let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n
@@ -283,6 +269,7 @@ let non_instantiated sigma =
*)
let real_clean env isevars ev args rhs =
+ let evd = ref isevars in
let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
let rec subs k t =
match kind_of_term t with
@@ -296,9 +283,11 @@ let real_clean env isevars ev args rhs =
subs k (existential_value isevars.evars (ev,args'))
else begin
let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in
- isevars.evars <- sigma;
- isevars.history <-
- (fst (destEvar rc),evar_source ev isevars)::isevars.history;
+ evd :=
+ {!evd with
+ evars = sigma;
+ history =
+ (fst (destEvar rc),evar_source ev isevars):: !evd.history};
rc
end
else
@@ -309,7 +298,7 @@ let real_clean env isevars ev args rhs =
let body = subs 0 rhs in
if not (closed0 body)
then error_not_clean env isevars.evars ev body (evar_source ev isevars);
- body
+ (!evd,body)
let make_evar_instance_with_rel env =
let n = rel_context_length (rel_context env) in
@@ -354,10 +343,17 @@ let new_isevar isevars env src typ =
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.evars <- sigma';
- isevars.history <- (fst (destEvar evar),src)::isevars.history;
+ {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
@@ -380,12 +376,12 @@ 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 evd = ise_map isevars ev in
+ let evi = ise_map isevars ev in
(* the bindings to invert *)
- let worklist = make_subst (evar_env evd) args in
- let body = real_clean env isevars ev worklist rhs in
- ise_define isevars ev body;
- [ev]
+ 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
+ isevars'',[ev]
(*-------------------*)
(* Auxiliary functions for the conversion algorithms modulo evars
@@ -466,7 +462,7 @@ let get_changed_pb isevars lev =
([],[])
isevars.conv_pbs
in
- isevars.conv_pbs <- pbs1;
+ {isevars with conv_pbs = pbs1},
pbs
(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
@@ -475,26 +471,28 @@ let get_changed_pb isevars lev =
* depend on these args). *)
let solve_refl conv_algo env isevars ev argsv1 argsv2 =
- if argsv1 = argsv2 then [] else
+ if argsv1 = argsv2 then (isevars,[]) else
let evd = Evd.map isevars.evars ev in
let hyps = evd.evar_hyps in
- let (_,rsign) =
+ let (isevars',_,rsign) =
array_fold_left2
- (fun (sgn,rsgn) a1 a2 ->
- if conv_algo env isevars CONV a1 a2 then
- (List.tl sgn, add_named_decl (List.hd sgn) rsgn)
+ (fun (isevars,sgn,rsgn) a1 a2 ->
+ let (isevars',b) = conv_algo env isevars CONV a1 a2 in
+ if b then
+ (isevars',List.tl sgn, add_named_decl (List.hd sgn) rsgn)
else
- (List.tl sgn, rsgn))
- (hyps,[]) argsv1 argsv2
+ (isevars,List.tl sgn, rsgn))
+ (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.evars <-
+ {isevars with
+ evars =
Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
- isevars.history <- (newev,evar_source ev isevars)::isevars.history;
+ history = (newev,evar_source ev isevars)::isevars.history},
[ev]
@@ -506,7 +504,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 lsp = match kind_of_term t2 with
+ let (isevars,lsp) = match kind_of_term t2 with
| Evar (n2,args2 as ev2)
when not (Evd.is_defined isevars.evars n2) ->
if n1 = n2 then
@@ -518,8 +516,11 @@ 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 pbs = get_changed_pb isevars lsp in
- List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
+ let (isevars,pbs) = get_changed_pb isevars 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)
+ pbs
(* Operations on value/type constraints *)
@@ -556,20 +557,21 @@ let mk_valcon c = Some c
let refine_evar_as_arrow isevars ev =
let (sigma,prod,evdom,evrng) = split_evar_to_arrow isevars.evars ev in
- evars_reset_evd sigma isevars;
let hst = evar_source (fst ev) isevars in
- isevars.history <- (fst evrng,hst)::(fst evdom, hst)::isevars.history;
- (prod,evdom,evrng)
+ 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 (prod,_,_) = refine_evar_as_arrow isevars ev in
- prod
+ let (isevars',prod,_,_) = refine_evar_as_arrow isevars ev in
+ isevars',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
+ evars_reset_evd sigma' isevars, destSort s
(* Propagation of constraints through application and abstraction:
@@ -578,15 +580,15 @@ let define_evar_as_sort isevars (ev,args) =
an evar instantiate it with the product of 2 new evars. *)
let split_tycon loc env isevars = function
- | None -> Anonymous,None,None
+ | None -> isevars,(Anonymous,None,None)
| Some c ->
let sigma = evars_of isevars in
let t = whd_betadeltaiota env sigma c in
match kind_of_term t with
- | Prod (na,dom,rng) -> na, Some dom, Some rng
+ | Prod (na,dom,rng) -> isevars, (na, Some dom, Some rng)
| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
- let (_,evdom,evrng) = refine_evar_as_arrow isevars ev in
- Anonymous, Some (mkEvar evdom), Some (mkEvar evrng)
+ let (isevars',_,evdom,evrng) = refine_evar_as_arrow isevars ev in
+ isevars',(Anonymous, Some (mkEvar evdom), Some (mkEvar evrng))
| _ -> 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 a08fb3f82..4223b0e78 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -52,14 +52,13 @@ val evars_of : evar_defs -> evar_map
val non_instantiated : evar_map -> (evar * evar_info) list
val create_evar_defs : evar_map -> evar_defs
-val evars_reset_evd : evar_map -> evar_defs -> unit
+val evars_reset_evd : evar_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_defs -> evar_constraint -> unit
+val add_conv_pb : evar_constraint -> evar_defs -> evar_defs
val is_defined_evar : evar_defs -> existential -> bool
-val ise_try : evar_defs -> (unit -> bool) list -> bool
val ise_undefined : evar_defs -> constr -> bool
val has_undefined_isevars : evar_defs -> constr -> bool
@@ -67,16 +66,21 @@ val new_isevar_sign :
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list ->
Evd.evar_map * Term.constr
-val new_isevar : evar_defs -> env -> loc * hole_kind -> constr -> constr
+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 is_eliminator : constr -> bool
val head_is_embedded_evar : evar_defs -> constr -> bool
val solve_simple_eqn :
- (env -> evar_defs -> conv_pb -> constr -> constr -> bool)
- -> env -> evar_defs -> conv_pb * existential * constr -> bool
+ (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
+ -> env -> evar_defs -> conv_pb * existential * constr ->
+ evar_defs * bool
-val define_evar_as_arrow : evar_defs -> existential -> types
-val define_evar_as_sort : evar_defs -> existential -> sorts
+val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
+val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
(* Value/Type constraints *)
@@ -95,7 +99,7 @@ val mk_valcon : constr -> val_constraint
val split_tycon :
loc -> env -> evar_defs -> type_constraint ->
- name * type_constraint * type_constraint
+ evar_defs * (name * type_constraint * type_constraint)
val valcon_of_tycon : type_constraint -> val_constraint
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dcb30c4d0..d0402a552 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -32,6 +32,23 @@ open Pattern
open Dyn
+let evd_comb0 f isevars =
+ let (evd',x) = f !isevars in
+ isevars := evd';
+ x
+let evd_comb1 f isevars x =
+ let (evd',y) = f !isevars x in
+ isevars := evd';
+ y
+let evd_comb2 f isevars x y =
+ let (evd',z) = f !isevars x y in
+ isevars := evd';
+ z
+let evd_comb3 f isevars x y z =
+ let (evd',t) = f !isevars x y z in
+ isevars := evd';
+ t
+
(************************************************************************)
(* This concerns Cases *)
open Declarations
@@ -147,24 +164,23 @@ let evar_type_fixpoint loc env isevars lna lar vdefj =
let lt = Array.length vdefj in
if Array.length lar = lt then
for i = 0 to lt-1 do
- if not (the_conv_x_leq env isevars
- (vdefj.(i)).uj_type
+ if not (e_cumul env isevars (vdefj.(i)).uj_type
(lift lt lar.(i))) then
- error_ill_typed_rec_body_loc loc env (evars_of isevars)
+ error_ill_typed_rec_body_loc loc env (evars_of !isevars)
i lna vdefj lar
done
let check_branches_message loc env isevars c (explft,lft) =
for i = 0 to Array.length explft - 1 do
- if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then
- let sigma = evars_of isevars in
+ if not (e_cumul env isevars lft.(i) explft.(i)) then
+ let sigma = evars_of !isevars in
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
done
(* coerce to tycon if any *)
let inh_conv_coerce_to_tycon loc env isevars j = function
| None -> j
- | Some typ -> inh_conv_coerce_to loc env isevars j typ
+ | Some typ -> evd_comb2 (inh_conv_coerce_to loc env) isevars j typ
let push_rels vars env = List.fold_right push_rel vars env
@@ -246,12 +262,12 @@ let rec pretype tycon env isevars lvar = function
| REvar (loc, ev, instopt) ->
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
- let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in
+ let hyps = (Evd.map (evars_of !isevars) ev).evar_hyps in
let args = match instopt with
| None -> instance_from_named_context hyps
| Some inst -> failwith "Evar subtitutions not implemented" in
let c = mkEvar (ev, args) in
- let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
inh_conv_coerce_to_tycon loc env isevars j tycon
| RPatVar (loc,(someta,n)) ->
@@ -260,8 +276,8 @@ let rec pretype tycon env isevars lvar = function
| RHole (loc,k) ->
(match tycon with
| Some ty ->
- { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
- | None -> error_unsolvable_implicit loc env (evars_of isevars) k)
+ { uj_val = e_new_isevar isevars env (loc,k) ty; uj_type = ty }
+ | None -> error_unsolvable_implicit loc env (evars_of !isevars) k)
| RRec (loc,fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
@@ -323,9 +339,9 @@ let rec pretype tycon env isevars lvar = function
| [] -> resj
| c::rest ->
let argloc = loc_of_rawconstr c in
- let resj = inh_app_fun env isevars resj in
+ let resj = evd_comb1 (inh_app_fun env) isevars resj in
let resty =
- whd_betadeltaiota env (evars_of isevars) resj.uj_type in
+ whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
let hj = pretype (mk_tycon c1) env isevars lvar c in
@@ -337,7 +353,7 @@ let rec pretype tycon env isevars lvar = function
| _ ->
let hj = pretype empty_tycon env isevars lvar c in
error_cant_apply_not_functional_loc
- (join_loc floc argloc) env (evars_of isevars)
+ (join_loc floc argloc) env (evars_of !isevars)
resj [hj]
in let resj = apply_rec env 1 fj args in
@@ -356,7 +372,7 @@ let rec pretype tycon env isevars lvar = function
inh_conv_coerce_to_tycon loc env isevars resj tycon
| RLambda(loc,name,c1,c2) ->
- let (name',dom,rng) = split_tycon loc env isevars tycon in
+ let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env isevars lvar c1 in
let var = (name,None,j.utj_val) in
@@ -385,10 +401,10 @@ let rec pretype tycon env isevars lvar = function
| RLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env (evars_of isevars) cj.uj_type
+ try find_rectype env (evars_of !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of isevars) cj
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj
in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 1 then
@@ -408,14 +424,14 @@ let rec pretype tycon env isevars lvar = function
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p isevars lvar p in
- let ccl = nf_evar (evars_of isevars) pj.utj_val in
+ let ccl = nf_evar (evars_of !isevars) pj.utj_val in
let psign = make_arity_signature env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
(Array.to_list cs.cs_concl_realargs)
@[build_dependent_constructor cs] in
let lp = lift cs.cs_nargs p in
- let fty = hnf_lam_applist env (evars_of isevars) lp inst in
+ let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
let fj = pretype (mk_tycon fty) env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
let v =
@@ -429,12 +445,12 @@ let rec pretype tycon env isevars lvar = function
let tycon = option_app (lift cs.cs_nargs) tycon in
let fj = pretype tycon env_f isevars lvar d in
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
- let ccl = nf_evar (evars_of isevars) fj.uj_type in
+ let ccl = nf_evar (evars_of !isevars) fj.uj_type in
let ccl =
if noccur_between 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
else
- error_cant_find_case_type_loc loc env (evars_of isevars)
+ error_cant_find_case_type_loc loc env (evars_of !isevars)
cj.uj_val in
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
@@ -448,10 +464,10 @@ let rec pretype tycon env isevars lvar = function
| ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle ->
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env (evars_of isevars) cj.uj_type
+ try find_rectype env (evars_of !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of isevars) cj
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj
in
let j = match po with
| Some p ->
@@ -459,16 +475,16 @@ let rec pretype tycon env isevars lvar = function
let dep = is_dependent_elimination env pj.uj_type indf in
let ar =
arity_of_case_predicate env indf dep (Type (new_univ())) in
- let _ = the_conv_x_leq env isevars pj.uj_type ar in
- let pj = j_nf_evar (evars_of isevars) pj in
+ let _ = e_cumul env isevars pj.uj_type ar in
+ let pj = j_nf_evar (evars_of !isevars) pj in
let pj = if dep then pj else make_dep_of_undep env indt pj in
let (bty,rsty) =
Indrec.type_rec_branches
- false env (evars_of isevars) indt pj.uj_val cj.uj_val
+ false env (evars_of !isevars) indt pj.uj_val cj.uj_val
in
if Array.length bty <> 1 then
error_number_branches_loc
- loc env (evars_of isevars) cj (Array.length bty);
+ loc env (evars_of !isevars) cj (Array.length bty);
let fj =
let tyc = bty.(0) in
pretype (mk_tycon tyc) env isevars lvar f
@@ -487,7 +503,7 @@ let rec pretype tycon env isevars lvar = function
(* get type information from type of branches *)
let expbr = Cases.branch_scheme env isevars false indf in
if Array.length expbr <> 1 then
- error_number_branches_loc loc env (evars_of isevars)
+ error_number_branches_loc loc env (evars_of !isevars)
cj (Array.length expbr);
let expti = expbr.(0) in
let fj = pretype (mk_tycon expti) env isevars lvar f in
@@ -500,32 +516,32 @@ let rec pretype tycon env isevars lvar = function
let arsgn = make_arity_signature env true indf in
let pred = lift (List.length arsgn) pred in
let pred =
- it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+ it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
arsgn in
false, pred
| None ->
- let sigma = evars_of isevars in
+ let sigma = evars_of !isevars in
error_cant_find_case_type_loc loc env sigma cj.uj_val
in
let ok, p =
try
let pred =
Cases.pred_case_ml
- env (evars_of isevars) false indt (0,fj.uj_type)
+ env (evars_of !isevars) false indt (0,fj.uj_type)
in
- if has_undefined_isevars isevars pred then
+ if has_undefined_isevars !isevars pred then
use_constraint ()
else
true, pred
with Cases.NotInferable _ ->
use_constraint ()
in
- let p = nf_evar (evars_of isevars) p in
+ let p = nf_evar (evars_of !isevars) p in
let (bty,rsty) =
Indrec.type_rec_branches
- false env (evars_of isevars) indt p cj.uj_val
+ false env (evars_of !isevars) indt p cj.uj_val
in
- let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+ let _ = option_app (e_cumul env isevars rsty) tycon in
let fj =
if ok then fj
else pretype (mk_tycon bty.(0)) env isevars lvar f
@@ -643,10 +659,10 @@ let rec pretype tycon env isevars lvar = function
| RIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env (evars_of isevars) cj.uj_type
+ try find_rectype env (evars_of !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
let cstrs = get_constructors env indf in
if Array.length cstrs <> 2 then
user_err_loc (loc,"",
@@ -661,13 +677,13 @@ let rec pretype tycon env isevars lvar = function
| Some p ->
let env_p = push_rels psign env in
let pj = pretype_type empty_valcon env_p isevars lvar p in
- let ccl = nf_evar (evars_of isevars) pj.utj_val in
+ let ccl = nf_evar (evars_of !isevars) pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
| None ->
let p = match tycon with
| Some ty -> ty
- | None -> new_isevar isevars env (loc,InternalHole) (new_Type ())
+ | None -> e_new_isevar isevars env (loc,InternalHole) (new_Type ())
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let f cs b =
@@ -680,8 +696,8 @@ let rec pretype tycon env isevars lvar = function
it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
- let pred = nf_evar (evars_of isevars) pred in
- let p = nf_evar (evars_of isevars) p in
+ let pred = nf_evar (evars_of !isevars) pred in
+ let p = nf_evar (evars_of !isevars) p in
let v =
let mis,_ = dest_ind_family indf in
let ci = make_default_case_info env IfStyle mis in
@@ -693,17 +709,17 @@ let rec pretype tycon env isevars lvar = function
let isrec = (st = MatchStyle) in
let cj = pretype empty_tycon env isevars lvar c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env (evars_of isevars) cj.uj_type
+ try find_rectype env (evars_of !isevars) cj.uj_type
with Not_found ->
let cloc = loc_of_rawconstr c in
- error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+ error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
let (dep,pj) = match po with
| Some p ->
let pj = pretype empty_tycon env isevars lvar p in
let dep = is_dependent_elimination env pj.uj_type indf in
let ar =
arity_of_case_predicate env indf dep (Type (new_univ())) in
- let _ = the_conv_x_leq env isevars pj.uj_type ar in
+ let _ = e_cumul env isevars pj.uj_type ar in
(dep, pj)
| None ->
(* get type information from type of branches *)
@@ -719,12 +735,12 @@ let rec pretype tycon env isevars lvar = function
let arsgn = make_arity_signature env true indf in
let pred = lift (List.length arsgn) pred in
let pred =
- it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+ it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
arsgn in
(true,
- Retyping.get_judgment_of env (evars_of isevars) pred)
+ Retyping.get_judgment_of env (evars_of !isevars) pred)
| None ->
- let sigma = evars_of isevars in
+ let sigma = evars_of !isevars in
error_cant_find_case_type_loc loc env sigma cj.uj_val
else
try
@@ -733,11 +749,11 @@ let rec pretype tycon env isevars lvar = function
pretype (mk_tycon expti) env isevars lvar lf.(i) in
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)
+ env (evars_of !isevars) isrec indt (i,fj.uj_type) in
+ if has_undefined_isevars !isevars pred then findtype (i+1)
else
let pty =
- Retyping.get_type_of env (evars_of isevars) pred in
+ Retyping.get_type_of env (evars_of !isevars) pred in
let pj = { uj_val = pred; uj_type = pty } in
(*
let _ = option_app (the_conv_x_leq env isevars pred) tycon
@@ -747,14 +763,14 @@ let rec pretype tycon env isevars lvar = function
with Cases.NotInferable _ -> findtype (i+1) in
findtype 0
in
- let pj = j_nf_evar (evars_of isevars) pj in
+ let pj = j_nf_evar (evars_of !isevars) pj in
let pj = if dep then pj else make_dep_of_undep env indt pj in
let (bty,rsty) =
Indrec.type_rec_branches
- isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in
- let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+ isrec env (evars_of !isevars) indt pj.uj_val cj.uj_val in
+ let _ = option_app (e_cumul env isevars rsty) tycon in
if Array.length bty <> Array.length lf then
- error_number_branches_loc loc env (evars_of isevars)
+ error_number_branches_loc loc env (evars_of !isevars)
cj (Array.length bty)
else
let lfj =
@@ -767,7 +783,7 @@ let rec pretype tycon env isevars lvar = function
let v =
if isrec
then
- transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt
+ transform_rec loc env (evars_of !isevars)(pj,cj.uj_val,lfv) indt
else
let mis,_ = dest_ind_family indf in
let ci = make_default_case_info env st mis in
@@ -785,7 +801,7 @@ let rec pretype tycon env isevars lvar = function
if isrec && mis_is_recursive_subset [tyi] recargs then
Some (Detyping.detype (false,env)
(ids_of_context env) (names_of_rel_context env)
- (nf_evar (evars_of isevars) v))
+ (nf_evar (evars_of !isevars) v))
else
(* Translate into a "match ... with" *)
let rtntypopt, indnalopt = match po with
@@ -902,7 +918,7 @@ let rec pretype tycon env isevars lvar = function
| RDynamic (loc,d) ->
if (tag d) = "constr" then
let c = constr_out d in
- let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
+ let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
j
(*inh_conv_coerce_to_tycon loc env isevars j tycon*)
else
@@ -914,39 +930,39 @@ and pretype_type valcon env isevars lvar = function
(match valcon with
| Some v ->
let s =
- let sigma = evars_of isevars in
+ let sigma = evars_of !isevars in
let t = Retyping.get_type_of env sigma v in
match kind_of_term (whd_betadeltaiota env sigma t) with
| Sort s -> s
| Evar v when is_Type (existential_type sigma v) ->
- define_evar_as_sort isevars v
+ evd_comb1 (define_evar_as_sort) isevars v
| _ -> anomaly "Found a type constraint which is not a type"
in
{ utj_val = v;
utj_type = s }
| None ->
let s = new_Type_sort () in
- { utj_val = new_isevar isevars env loc (mkSort s);
+ { utj_val = e_new_isevar isevars env loc (mkSort s);
utj_type = s})
| c ->
let j = pretype empty_tycon env isevars lvar c in
- let tj = inh_coerce_to_sort env isevars j in
+ let tj = evd_comb1 (inh_coerce_to_sort env) isevars j in
match valcon with
| None -> tj
| Some v ->
- if the_conv_x_leq env isevars v tj.utj_val then tj
+ if e_cumul env isevars v tj.utj_val then tj
else
error_unexpected_type_loc
- (loc_of_rawconstr c) env (evars_of isevars) tj.utj_val v
+ (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
let unsafe_infer tycon isevars env lvar constr =
let j = pretype tycon env isevars lvar constr in
- j_nf_evar (evars_of isevars) j
+ j_nf_evar (evars_of !isevars) j
let unsafe_infer_type valcon isevars env lvar constr =
let tj = pretype_type valcon env isevars lvar constr in
- tj_nf_evar (evars_of isevars) tj
+ tj_nf_evar (evars_of !isevars) tj
(* If fail_evar is false, [process_evars] builds a meta_map with the
unresolved Evar that were not in initial sigma; otherwise it fail
@@ -958,14 +974,14 @@ let unsafe_infer_type valcon isevars env lvar constr =
(* assumes the defined existentials have been replaced in c (should be
done in unsafe_infer and unsafe_infer_type) *)
let check_evars fail_evar env initial_sigma isevars c =
- let sigma = evars_of isevars in
+ let sigma = evars_of !isevars in
let rec proc_rec c =
match kind_of_term c with
| Evar (ev,args as k) ->
assert (Evd.in_dom sigma ev);
if not (Evd.in_dom initial_sigma ev) then
(if fail_evar then
- let (loc,k) = evar_source ev isevars in
+ let (loc,k) = evar_source ev !isevars in
error_unsolvable_implicit loc env sigma k)
| _ -> iter_constr proc_rec c
in
@@ -980,10 +996,10 @@ let check_evars fail_evar env initial_sigma isevars c =
type open_constr = evar_map * constr
let ise_resolve_casted_gen fail_evar sigma env lvar typ c =
- let isevars = create_evar_defs sigma in
+ let isevars = ref (create_evar_defs sigma) in
let j = unsafe_infer (mk_tycon typ) isevars env lvar c in
check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
- (evars_of isevars, j)
+ (evars_of !isevars, j)
let ise_resolve_casted sigma env typ c =
ise_resolve_casted_gen true sigma env ([],[]) typ c
@@ -993,16 +1009,16 @@ let ise_resolve_casted sigma env typ c =
allows us to extend env with some bindings *)
let ise_infer_gen fail_evar sigma env lvar exptyp c =
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
- let isevars = create_evar_defs sigma in
+ let isevars = ref (create_evar_defs sigma) in
let j = unsafe_infer tycon isevars env lvar c in
check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
- (evars_of isevars, j)
+ (evars_of !isevars, j)
let ise_infer_type_gen fail_evar sigma env lvar c =
- let isevars = create_evar_defs sigma in
+ let isevars = ref (create_evar_defs sigma) in
let tj = unsafe_infer_type empty_valcon isevars env lvar c in
check_evars fail_evar env sigma isevars tj.utj_val;
- (evars_of isevars, tj)
+ (evars_of !isevars, tj)
type var_map = (identifier * unsafe_judgment) list
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3d88422eb..57a3d1be8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -71,12 +71,12 @@ val constr_out : Dyn.t -> constr
* Unused outside, but useful for debugging
*)
val pretype :
- type_constraint -> env -> evar_defs ->
+ type_constraint -> env -> evar_defs ref ->
var_map * (identifier * identifier option) list ->
rawconstr -> unsafe_judgment
val pretype_type :
- val_constraint -> env -> evar_defs ->
+ val_constraint -> env -> evar_defs ref ->
var_map * (identifier * identifier option) list ->
rawconstr -> unsafe_type_judgment
(*i*)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index aea164a9b..83377449d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,7 +49,7 @@ let abstract_list_all env sigma typ c l =
(*******************************)
-type maps = evar_map * meta_map
+type maps = evar_defs * meta_map
(* [w_Define evd sp c]
*
@@ -59,18 +59,22 @@ type maps = evar_map * meta_map
* No unification is performed in order to assert that [c] has the
* correct type.
*)
-let w_Define sp c evd =
+let w_Define sp c (evd,mmap) =
let sigma = evars_of evd in
if Evd.is_defined sigma sp then
error "Unify.w_Define: cannot define evar twice";
let spdecl = Evd.map sigma sp in
let env = evar_env spdecl in
let _ =
- try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
- with Not_found ->
- error "Instantiation contains unlegal variables" in
+ try Typing.mcheck env (Evd.rmv sigma sp,Metamap.empty) c spdecl.evar_concl
+ with
+ Not_found -> error "Instantiation contains unlegal variables"
+ | (Type_errors.TypeError (e, Type_errors.UnboundVar v))->
+ errorlabstrm "w_Define"
+ (str "Cannot use variable " ++ pr_id v ++ str " to define " ++
+ str (string_of_existential sp)) in
let spdecl' = { spdecl with evar_body = Evar_defined c } in
- evars_reset_evd (Evd.add sigma sp spdecl') evd
+ (evars_reset_evd (Evd.add sigma sp spdecl') evd, mmap)
(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -194,21 +198,20 @@ let unify_0 env sigma cv_pb m n =
* close it off. But this might not always work,
* since other metavars might also need to be resolved. *)
-let applyHead env sigma n c =
- let evd = create_evar_defs sigma in
- let rec apprec n c cty =
+let applyHead env evd n c =
+ let rec apprec n c cty evd =
if n = 0 then
- (evars_of evd, c)
+ (evd, c)
else
match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
| Prod (_,c1,c2) ->
- let evar =
+ let (evd',evar) =
Evarutil.new_isevar evd env
(dummy_loc,Rawterm.InternalHole) c1 in
- apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2)
+ apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
| _ -> error "Apply_Head_Then"
in
- apprec n c (Typing.type_of env (evars_of evd) c)
+ apprec n c (Typing.type_of env (evars_of evd) c) evd
let is_mimick_head f =
match kind_of_term f with
@@ -219,19 +222,17 @@ let is_mimick_head f =
or in evars, possibly generating new unification problems; if [b]
is true, unification of types of metas is required *)
-let w_merge env with_types metas evars (sigma,metamap) =
- let evd = create_evar_defs sigma in
- let mmap = ref metamap in
+let w_merge env with_types metas evars maps =
let ty_metas = ref [] in
let ty_evars = ref [] in
- let rec w_merge_rec metas evars =
+ let rec w_merge_rec (evd,mmap as maps) metas evars =
match (evars,metas) with
- | ([], []) -> ()
+ | ([], []) -> maps
| ((lhs,rhs)::t, metas) ->
(match kind_of_term rhs with
- | Meta k -> w_merge_rec ((k,lhs)::metas) t
+ | Meta k -> w_merge_rec maps ((k,lhs)::metas) t
| krhs ->
(match kind_of_term lhs with
@@ -240,7 +241,7 @@ let w_merge env with_types metas evars (sigma,metamap) =
if is_defined_evar evd ev then
let (metas',evars') =
unify_0 env (evars_of evd) CONV rhs lhs in
- w_merge_rec (metas'@metas) (evars'@t)
+ w_merge_rec maps (metas'@metas) (evars'@t)
else begin
let rhs' =
if occur_meta rhs then subst_meta metas rhs else rhs
@@ -250,60 +251,59 @@ let w_merge env with_types metas evars (sigma,metamap) =
match krhs with
| App (f,cl) when is_mimick_head f ->
(try
- w_Define evn rhs' evd;
- w_merge_rec metas t
+ w_merge_rec (w_Define evn rhs' maps) metas t
with ex when precatchable_exception ex ->
- mimick_evar f (Array.length cl) evn;
- w_merge_rec metas evars)
+ let maps' =
+ mimick_evar maps f (Array.length cl) evn in
+ w_merge_rec maps' metas evars)
| _ ->
(* ensure tail recursion in non-mimickable case! *)
- w_Define evn rhs' evd;
- w_merge_rec metas t
+ w_merge_rec (w_Define evn rhs' maps) metas t
end
| _ -> anomaly "w_merge_rec"))
| ([], (mv,n)::t) ->
- if meta_defined !mmap mv then
+ if meta_defined mmap mv then
let (metas',evars') =
- unify_0 env (evars_of evd) CONV (meta_fvalue !mmap mv).rebus n in
- w_merge_rec (metas'@t) evars'
+ unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in
+ w_merge_rec maps (metas'@t) evars'
else
begin
if with_types (* or occur_meta mvty *) then
- (let mvty = meta_type !mmap mv in
+ (let mvty = meta_type mmap mv in
try
let sigma = evars_of evd in
(* why not typing with the metamap ? *)
- let nty = Typing.type_of env sigma (nf_meta !mmap n) in
+ let nty = Typing.type_of env sigma (nf_meta mmap n) in
let (mc,ec) = unify_0 env sigma CUMUL nty mvty in
ty_metas := mc @ !ty_metas;
ty_evars := ec @ !ty_evars
with e when precatchable_exception e -> ());
- mmap := meta_assign mv n !mmap;
- w_merge_rec t []
+ let mmap' = meta_assign mv n mmap in
+ w_merge_rec (evd,mmap') t []
end
- and mimick_evar hdc nargs sp =
+
+ and mimick_evar (evd,mmap) hdc nargs sp =
let ev = Evd.map (evars_of evd) sp in
let sp_env = Global.env_of_context ev.evar_hyps in
- let (sigma', c) = applyHead sp_env (evars_of evd) nargs hdc in
- evars_reset_evd sigma' evd;
+ let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =
- unify_0 sp_env (evars_of evd) CUMUL
- (Retyping.get_type_of sp_env (evars_of evd) c) ev.evar_concl in
- w_merge_rec mc ec;
- if sigma'== (evars_of evd)
- then w_Define sp c evd
- else w_Define sp (Evarutil.nf_evar (evars_of evd) c) evd in
+ unify_0 sp_env (evars_of evd') CUMUL
+ (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
+ let maps' = w_merge_rec (evd',mmap) mc ec in
+ if (evars_of evd') == (evars_of (fst maps'))
+ then w_Define sp c maps'
+ else w_Define sp (Evarutil.nf_evar (evars_of (fst maps')) c) maps' in
(* merge constraints *)
- w_merge_rec metas evars;
- (if with_types then
+ let maps' = w_merge_rec maps metas evars in
+ if with_types then
(* merge constraints about types: if they fail, don't worry *)
- try w_merge_rec !ty_metas !ty_evars
-(* TODO: should backtrack *)
- with e when precatchable_exception e -> ());
- (evars_of evd, !mmap)
+ try w_merge_rec maps' !ty_metas !ty_evars
+ with e when precatchable_exception e -> maps'
+ else
+ maps'
(* [w_unify env evd M N]
performs a unification of M and N, generating a bunch of
@@ -316,7 +316,7 @@ let w_merge env with_types metas evars (sigma,metamap) =
types of metavars are unifiable with the types of their instances *)
let w_unify_core_0 env with_types cv_pb m n evd =
- let (mc,ec) = unify_0 env (fst evd) cv_pb m n in
+ let (mc,ec) = unify_0 env (evars_of (fst evd)) cv_pb m n in
w_merge env with_types mc ec evd
let w_unify_0 env = w_unify_core_0 env false
@@ -419,7 +419,7 @@ let w_unify_to_subterm_list env allow_K oplist t evd =
(evd,[])
let secondOrderAbstraction env allow_K typ (p, oplist) evd =
- let sigma = fst evd in
+ let sigma = evars_of (fst evd) in
let (evd',cllist) =
w_unify_to_subterm_list env allow_K oplist typ evd in
let typp = meta_type (snd evd') p in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index d05b8cb5a..f033c9e87 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,11 +15,12 @@ open Term
open Sign
open Environ
open Evd
+open Evarutil
(*i*)
-type maps = evar_map * meta_map
+type maps = evar_defs * meta_map
-val w_Define : evar -> constr -> Evarutil.evar_defs -> unit
+val w_Define : evar -> constr -> maps -> maps
(* The "unique" unification fonction *)
val w_unify :
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 2b33d142f..27ae5ebd9 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -17,6 +17,7 @@ open Termops
open Sign
open Environ
open Evd
+open Evarutil
open Proof_type
open Refiner
open Proof_trees
@@ -69,29 +70,29 @@ let clenv_cast_meta clenv =
crec
-let clenv_refine kONT clenv gls =
+let clenv_refine clenv gls =
tclTHEN
- (kONT clenv.hook)
+ (tclEVARS clenv.hook.sigma)
(refine (clenv_instance_template clenv)) gls
-let clenv_refine_cast kONT clenv gls =
+let clenv_refine_cast clenv gls =
tclTHEN
- (kONT clenv.hook)
+ (tclEVARS clenv.hook.sigma)
(refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
gls
-let res_pf kONT clenv gls =
- clenv_refine kONT (clenv_unique_resolver false clenv gls) gls
+let res_pf clenv gls =
+ clenv_refine (clenv_unique_resolver false clenv gls) gls
-let res_pf_cast kONT clenv gls =
- clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
+let res_pf_cast clenv gls =
+ clenv_refine_cast (clenv_unique_resolver false clenv gls) gls
-let elim_res_pf kONT clenv allow_K gls =
- clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
+let elim_res_pf clenv allow_K gls =
+ clenv_refine_cast (clenv_unique_resolver allow_K clenv gls) gls
-let elim_res_pf_THEN_i kONT clenv tac gls =
+let elim_res_pf_THEN_i clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
- tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
+ tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
(* [clenv_pose_dependent_evars clenv]
* For each dependent evar in the clause-env which does not have a value,
@@ -103,7 +104,7 @@ let clenv_pose_dependent_evars clenv =
let dep_mvs = clenv_dependent false clenv in
List.fold_left
(fun clenv mv ->
- let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
+ let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
let (evar_n,_) = destEvar evar in
let tY = clenv_instance_type clenv mv in
let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
@@ -111,8 +112,8 @@ let clenv_pose_dependent_evars clenv =
clenv
dep_mvs
-let e_res_pf kONT clenv gls =
- clenv_refine kONT
+let e_res_pf clenv gls =
+ clenv_refine
(clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
@@ -125,9 +126,9 @@ let e_res_pf kONT clenv gls =
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unifyTerms m n gls =
let env = pf_env gls in
- let sigma = project gls in
- tclIDTAC {it = gls.it;
- sigma = fst (Unification.w_unify false env CONV m n (sigma,Evd.Metamap.empty))}
+ let maps = (create_evar_defs (project gls), Evd.Metamap.empty) in
+ let maps' = Unification.w_unify false env CONV m n maps in
+ tclIDTAC {it = gls.it; sigma = evars_of (fst maps')}
let unify m gls =
let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 1dd14e773..1695db2f5 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -20,10 +20,9 @@ open Proof_type
(* Tactics *)
val unify : constr -> tactic
-val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic
-val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf_THEN_i :
- (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
+val clenv_refine : wc clausenv -> tactic
+val res_pf : wc clausenv -> tactic
+val res_pf_cast : wc clausenv -> tactic
+val elim_res_pf : wc clausenv -> bool -> tactic
+val e_res_pf : wc clausenv -> tactic
+val elim_res_pf_THEN_i : wc clausenv -> (wc clausenv -> tactic array) -> tactic
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d8dfb7d59..2e2060349 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -30,23 +30,10 @@ open Nameops
type wc = named_context sigma (* for a better reading of the following *)
-let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
type w_tactic = named_context sigma -> named_context sigma
-let startWalk gls =
- let evc = project_with_focus gls in
- (evc,
- (fun wc' gls' ->
- if not !Options.debug or (gls.it = gls'.it) then
-(* if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*)
- tclIDTAC {it=gls'.it; sigma = (get_gc wc')}
-(* else
- (local_Constraints (get_focus (ids_it wc'))
- {it=gls'.it; sigma = get_gc (ids_it wc')})*)
- else error "Walking"))
-
let extract_decl sp evc =
let evdmap = evc.sigma in
let evd = Evd.map evdmap sp in
@@ -56,76 +43,12 @@ let extract_decl sp evc =
let restore_decl sp evd evc =
(rc_add evc (sp,evd))
-
-(* [w_Focusing sp wt wc]
- *
- * Focuses the walking context WC onto the declaration SP, given that
- * this declaration is UNDEFINED. Then, it runs the walking_tactic,
- * WT, on this new context. When the result is returned, we recover
- * the resulting focus (access list) and restore it to SP's declaration.
- *
- * It is an error to cause SP to change state while we are focused on it. *)
-
-(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
- (wc : named_context sigma) =
- let hyps = wc.it
- and evd = Evd.map wc.sigma sp in
- let (wc' : named_context sigma) = extract_decl sp wc in
- let (wc'',rslt) = wt wc' in
-(* if not (ids_eq wc wc'') then error "w_saving_focus"; *)
- if wc'==wc'' then
- wt' rslt wc
- else
- let wc''' = restore_decl sp evd wc'' in
- wt' rslt {it = hyps; sigma = wc'''.sigma} *)
-
-let w_add_sign (id,t) (wc : named_context sigma) =
- { it = Sign.add_named_decl (id,None,t) wc.it;
- sigma = wc.sigma }
-
-let w_Focus sp wc = extract_decl sp wc
-
-let w_Underlying wc = wc.sigma
-let w_whd wc c = Evarutil.whd_castappevar (w_Underlying wc) c
-let w_type_of wc c =
- type_of (Global.env_of_context wc.it) wc.sigma c
-let w_env wc = get_env wc
-let w_hyps wc = named_context (get_env wc)
-let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k
-let w_const_value wc = constant_value (w_env wc)
-let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n
-let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
-let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c
-
-
let w_Declare sp ty (wc : named_context sigma) =
- let _ = w_type_of wc ty in (* Utile ?? *)
+ let _ = Typing.type_of (get_env wc) wc.sigma ty in (* Utile ?? *)
let sign = get_hyps wc in
let newdecl = mk_goal sign ty in
((rc_add wc (sp,newdecl)): named_context sigma)
-let w_Define sp c wc =
- let spdecl = Evd.map (w_Underlying wc) sp in
- let cty =
- try
- w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl))
- with
- Not_found -> error "Instantiation contains unlegal variables"
- | (Type_errors.TypeError (e, Type_errors.UnboundVar v))->
- errorlabstrm "w_Define"
- (str "Cannot use variable " ++ pr_id v ++ str " to define " ++
- str (string_of_existential sp))
- in
- match spdecl.evar_body with
- | Evar_empty ->
- let spdecl' = { evar_hyps = spdecl.evar_hyps;
- evar_concl = spdecl.evar_concl;
- evar_body = Evar_defined c }
- in
- Proof_trees.rc_add wc (sp,spdecl')
- | _ -> error "define_evar"
-
-
(******************************************)
(* Instantiation of existential variables *)
(******************************************)
@@ -151,7 +74,7 @@ let w_refine ev rawc wc =
let instantiate_pf_com n com pfts =
let gls = top_goal_of_pftreestate pfts in
let wc = project_with_focus gls in
- let sigma = (w_Underlying wc) in
+ let sigma = wc.sigma in
let (sp,evd) (* as evc *) =
try
List.nth (Evarutil.non_instantiated sigma) (n-1)
@@ -162,5 +85,4 @@ let instantiate_pf_com n com pfts =
let env = Evarutil.evar_env e_info in
let rawc = Constrintern.interp_rawconstr sigma env com in
let wc' = w_refine sp rawc wc in
- let newgc = (w_Underlying wc') in
- change_constraints_pftreestate newgc pfts
+ change_constraints_pftreestate wc'.sigma pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 049c6594e..54646caf8 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -22,7 +22,6 @@ type wc = named_context sigma (* for a better reading of the following *)
(* Refinement of existential variables. *)
-val rc_of_pfsigma : proof_tree sigma -> wc
val rc_of_glsigma : goal sigma -> wc
(* A [w_tactic] is a tactic which modifies the a set of evars of which
@@ -30,28 +29,11 @@ val rc_of_glsigma : goal sigma -> wc
dependent goal *)
type w_tactic = wc -> wc
-val startWalk : goal sigma -> wc * (wc -> tactic)
-
-val extract_decl : evar -> w_tactic
-val restore_decl : evar -> evar_info -> w_tactic
val w_Declare : evar -> types -> w_tactic
-val w_Define : evar -> constr -> w_tactic
-
-val w_Underlying : wc -> evar_map
-val w_env : wc -> env
-val w_hyps : wc -> named_context
-val w_whd : wc -> constr -> constr
-val w_type_of : wc -> constr -> constr
-val w_add_sign : (identifier * types) -> w_tactic
-
-val w_whd_betadeltaiota : wc -> constr -> constr
-val w_hnf_constr : wc -> constr -> constr
-val w_conv_x : wc -> constr -> constr -> bool
-val w_const_value : wc -> constant -> constr
-val w_defined_evar : wc -> existential_key -> bool
val w_refine : evar -> Rawterm.rawconstr -> w_tactic
-val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+val instantiate_pf_com :
+ int -> Topconstr.constr_expr -> pftreestate -> pftreestate
(* the instantiate tactic was moved to tactics/evar_tactics.ml *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a0053d8a1..b2629013b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -257,12 +257,6 @@ let vernac_tactic (s,args) =
let tacfun = lookup_tactic s args in
abstract_extended_tactic s args tacfun
-(* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
-let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
-
-(* [rc_of_glsigma : proof sigma -> readable_constraints] *)
-let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
-
(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
where pfterm is the constr corresponding to the proof
@@ -1027,3 +1021,6 @@ let tclINFO (tac : tactic) gls =
msgnl (hov 0 (str "Info failed to apply validation"))
end;
res
+
+(* Change evars *)
+let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index f9c0c71d5..f6f65ef93 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -68,6 +68,8 @@ val frontier_mapi :
val tclIDTAC : tactic
val tclIDTAC_MESSAGE : string -> tactic
+(* [tclEVARS sigma] changes the current evar map *)
+val tclEVARS : evar_map -> tactic
(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fc9bd3aa2..700c8fed7 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -41,10 +41,9 @@ let e_assumption gl =
tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
let e_resolve_with_bindings_tac (c,lbind) gl =
- let (wc,kONT) = startWalk gl in
- let t = w_hnf_constr wc (w_type_of wc c) in
- let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in
- Clenvtac.e_res_pf kONT clause gl
+ let t = pf_hnf_constr gl (pf_type_of gl c) in
+ let clause = make_clenv_binding_apply (rc_of_glsigma gl) (-1) (c,t) lbind in
+ Clenvtac.e_res_pf clause gl
let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bfedc8220..38dc8f58e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -567,10 +567,10 @@ 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 = Evarutil.create_evar_defs sigma in
+ let isevars = ref (Evarutil.create_evar_defs sigma) in
let rec sigrec_clausal_form siglen p_i =
if siglen = 0 then
- if Evarconv.the_conv_x env isevars p_i dFLTty then
+ if Evarconv.e_conv env isevars p_i dFLTty then
(* the_conv_x had a side-effect on isevars *)
dFLT
else
@@ -579,19 +579,19 @@ 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.new_isevar isevars env (dummy_loc,InternalHole)
+ let ev = Evarutil.e_new_isevar isevars env (dummy_loc,InternalHole)
(Evarutil.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 (Evarutil.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 (Evarutil.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/inv.ml b/tactics/inv.ml
index e74fc05a9..7c4456b3d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -445,9 +445,8 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
let raw_inversion inv_kind indbinding id status names gl =
let env = pf_env gl and sigma = project gl in
let c = mkVar id in
- let (wc,kONT) = startWalk gl in
let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
- let indclause = mk_clenv_from wc (c,t) in
+ let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in
let indclause' = clenv_constrain_with_bindings indbinding indclause in
let newc = clenv_instance_template indclause' in
let ccl = clenv_instance_template_type indclause' in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 95546142f..118481547 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -287,10 +287,9 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
- let (wc,kONT) = startWalk gls in
- let clause = mk_clenv_type_of wc c in
+ let clause = mk_clenv_type_of (rc_of_glsigma gls) c in
let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
- Clenvtac.elim_res_pf kONT clause true gls
+ Clenvtac.elim_res_pf clause true gls
with
| UserError (a,b) ->
errorlabstrm "LemInv"
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index b8b0cf9ac..195ba3c61 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -886,10 +886,10 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
*)
let general_s_rewrite lft2rgt c gl =
- let (wc,_) = Evar_refiner.startWalk gl in
let ctype = pf_type_of gl c in
let eqclause =
- Clenv.make_clenv_binding wc (c,ctype) Rawterm.NoBindings in
+ Clenv.make_clenv_binding
+ (Evar_refiner.rc_of_glsigma gl) (c,ctype) Rawterm.NoBindings in
let (equiv, args) =
decompose_app (Clenv.clenv_instance_template_type eqclause) in
let rec get_last_two = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 0e10a0b5d..72ec0bd2e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,10 +324,9 @@ let general_elim_then_using
elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
(* applying elimination_scheme just a little modified *)
- let (wc,kONT) = startWalk gl in
- let indclause = mk_clenv_from wc (c,t) in
+ let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in
let indclause' = clenv_constrain_with_bindings indbindings indclause in
- let elimclause = mk_clenv_from () (elim,w_type_of wc elim) in
+ let elimclause = mk_clenv_from () (elim,pf_type_of gl elim) in
let indmv =
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
| Meta mv -> mv
@@ -371,7 +370,7 @@ let general_elim_then_using
| None -> elimclause'
| Some p -> clenv_assign pmv p elimclause'
in
- elim_res_pf_THEN_i kONT elimclause' branchtacs gl
+ elim_res_pf_THEN_i elimclause' branchtacs gl
let elimination_then_using tac predicate (indbindings,elimbindings) c gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d5d972111..6fe3d75af 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -442,20 +442,20 @@ let apply_with_bindings (c,lbind) gl =
| Lambda _ -> Clenvtac.res_pf_cast
| _ -> Clenvtac.res_pf
in
- let (wc,kONT) = startWalk gl in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
- let thm_ty0 = nf_betaiota (w_type_of wc c) in
+ let wc = rc_of_glsigma gl in
+ let thm_ty0 = nf_betaiota (pf_type_of gl c) in
let rec try_apply thm_ty =
try
let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
if n<0 then error "Apply: theorem has not enough premisses.";
let clause = make_clenv_binding_apply wc n (c,thm_ty) lbind in
- apply kONT clause gl
+ apply clause gl
with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
let red_thm =
- try red_product (w_env wc) (w_Underlying wc) thm_ty
+ try red_product (pf_env gl) (project gl) thm_ty
with (Redelimination | UserError _) -> raise exn in
try_apply red_thm in
try try_apply thm_ty0
@@ -463,7 +463,7 @@ let apply_with_bindings (c,lbind) gl =
(* Last chance: if the head is a variable, apply may try
second order unification *)
let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in
- apply kONT clause gl
+ apply clause gl
let apply c = apply_with_bindings (c,NoBindings)
@@ -474,9 +474,8 @@ let apply_list = function
(* Resolution with no reduction on the type *)
let apply_without_reduce c gl =
- let (wc,kONT) = startWalk gl in
- let clause = mk_clenv_type_of wc c in
- res_pf kONT clause gl
+ let clause = mk_clenv_type_of (rc_of_glsigma gl) c in
+ res_pf clause gl
(* A useful resolution tactic which, if c:A->B, transforms |- C into
|- B -> C and |- A
@@ -831,8 +830,8 @@ let rec intros_clearing = function
(* Adding new hypotheses *)
let new_hyp mopt (c,lbind) g =
- let (wc,kONT) = startWalk g in
- let clause = make_clenv_binding wc (c,w_type_of wc c) lbind in
+ let clause =
+ make_clenv_binding (rc_of_glsigma g) (c,pf_type_of g c) lbind in
let (thd,tstack) = whd_stack (clenv_instance_template clause) in
let nargs = List.length tstack in
let cut_pf =
@@ -841,7 +840,7 @@ let new_hyp mopt (c,lbind) g =
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
in
- (tclTHENLAST (tclTHEN (kONT clause.hook)
+ (tclTHENLAST (tclTHEN (tclEVARS clause.hook.sigma)
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
@@ -896,19 +895,11 @@ let simplest_split = split NoBindings
(* Elimination tactics *)
(********************************************)
-
-(* kONT : ??
- * wc : ??
- * elimclause : ??
- * inclause : ??
- * gl : the current goal
-*)
-
let last_arg c = match kind_of_term c with
| App (f,cl) -> array_last cl
| _ -> anomaly "last_arg"
-let elimination_clause_scheme kONT elimclause indclause allow_K gl =
+let elimination_clause_scheme elimclause indclause allow_K gl =
let indmv =
(match kind_of_term (last_arg (clenv_template elimclause).rebus) with
| Meta mv -> mv
@@ -916,7 +907,7 @@ let elimination_clause_scheme kONT elimclause indclause allow_K gl =
(str "The type of elimination clause is not well-formed"))
in
let elimclause' = clenv_fchain indmv elimclause indclause in
- elim_res_pf kONT elimclause' allow_K gl
+ elim_res_pf elimclause' allow_K gl
(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and
* refine fails *)
@@ -933,13 +924,13 @@ let type_clenv_binding wc (c,t) lbind =
*)
let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl =
- let (wc,kONT) = startWalk gl in
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let indclause = make_clenv_binding wc (c,t) lbindc in
- let elimt = w_type_of wc elimc in
- let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in
- elimination_clause_scheme kONT elimclause indclause allow_K gl
+ let indclause = make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc in
+ let elimt = pf_type_of gl elimc in
+ let elimclause =
+ make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in
+ elimination_clause_scheme elimclause indclause allow_K gl
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
@@ -980,7 +971,7 @@ let simplest_elim c = default_elim (c,NoBindings)
(* Elimination in hypothesis *)
-let elimination_in_clause_scheme kONT id elimclause indclause =
+let elimination_in_clause_scheme id elimclause indclause =
let (hypmv,indmv) =
match clenv_independent elimclause with
[k1;k2] -> (k1,k2)
@@ -998,7 +989,7 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id);
tclTHEN
- (kONT elimclause''.hook)
+ (tclEVARS elimclause''.hook.sigma)
(tclTHENS
(cut new_hyp_typ)
[ (* Try to insert the new hyp at the same place *)
@@ -1007,13 +998,14 @@ let elimination_in_clause_scheme kONT id elimclause indclause =
refine_no_check new_hyp_prf])
let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
- let (wc,kONT) = startWalk gl in
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let indclause = make_clenv_binding wc (c,t) lbindc in
- let elimt = w_type_of wc elimc in
- let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in
- elimination_in_clause_scheme kONT id elimclause indclause gl
+ let indclause =
+ make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc in
+ let elimt = pf_type_of gl elimc in
+ let elimclause =
+ make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in
+ elimination_in_clause_scheme id elimclause indclause gl
(* Case analysis tactics *)
@@ -1384,11 +1376,11 @@ let cook_sign hyp0 indvars env =
let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
let c = mkVar varname in
- let (wc,kONT) = startWalk gl in
+ let wc = rc_of_glsigma gl in
let indclause = make_clenv_binding wc (c,typ) NoBindings in
let elimclause =
make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
- elimination_clause_scheme kONT elimclause indclause true gl
+ elimination_clause_scheme elimclause indclause true gl
let make_up_names7 n ind (old_style,cname) =
if old_style (* = V6.3 version of Induction on hypotheses *)
@@ -1675,14 +1667,13 @@ let simple_destruct = function
*)
let elim_scheme_type elim t gl =
- let (wc,kONT) = startWalk gl in
- let clause = mk_clenv_type_of wc elim in
+ let clause = mk_clenv_type_of (rc_of_glsigma gl) elim in
match kind_of_term (last_arg (clenv_template clause).rebus) with
| Meta mv ->
let clause' =
(* t is inductive, then CUMUL or CONV is irrelevant *)
clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
- elim_res_pf kONT clause' true gl
+ elim_res_pf clause' true gl
| _ -> anomaly "elim_scheme_type"
let elim_type t gl =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 03:55:02 +0000