diff options
author | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 15:56:10 +0000 |
---|---|---|
committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-12 15:56:10 +0000 |
commit | ecb17841e955ca888010d72876381a86cdcf09ad (patch) | |
tree | 4c6c24f6ce5a8221f8632fceb0f6717948cdca8d | |
parent | 2f611e10fb3dc42fc00d80b1e087fa33f6fc846e (diff) |
Suppression des stamps et donc des *_constraints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 89 | ||||
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | contrib/interface/showproof.ml | 1 | ||||
-rwxr-xr-x | contrib/interface/showproof.mli | 1 | ||||
-rw-r--r-- | proofs/clenv.ml | 2 | ||||
-rw-r--r-- | proofs/clenv.mli | 11 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 76 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 40 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 44 | ||||
-rw-r--r-- | proofs/proof_trees.mli | 23 | ||||
-rw-r--r-- | proofs/proof_type.ml | 7 | ||||
-rw-r--r-- | proofs/proof_type.mli | 7 | ||||
-rw-r--r-- | proofs/refiner.ml | 27 | ||||
-rw-r--r-- | proofs/refiner.mli | 21 | ||||
-rw-r--r-- | proofs/tacmach.ml | 4 | ||||
-rw-r--r-- | proofs/tacmach.mli | 20 | ||||
-rw-r--r-- | tactics/tacticals.ml | 2 | ||||
-rw-r--r-- | tactics/tactics.ml | 1 | ||||
-rw-r--r-- | tactics/tactics.mli | 3 | ||||
-rw-r--r-- | tactics/wcclausenv.ml | 2 | ||||
-rw-r--r-- | tactics/wcclausenv.mli | 2 |
21 files changed, 164 insertions, 223 deletions
@@ -135,8 +135,8 @@ pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi \ pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi proofs/tacmach.cmi kernel/term.cmi \ - lib/util.cmi + pretyping/reductionops.cmi kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi @@ -147,11 +147,10 @@ proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ - kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi + kernel/sign.cmi kernel/term.cmi lib/util.cmi proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pretyping.cmi lib/stamps.cmi pretyping/tacred.cmi \ - kernel/term.cmi lib/util.cmi + pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi proofs/refiner.cmi: pretyping/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ @@ -197,8 +196,8 @@ tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \ tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ - kernel/term.cmi + kernel/sign.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + tactics/tacticals.cmi kernel/term.cmi tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \ @@ -303,8 +302,8 @@ contrib/interface/showproof.cmi: contrib/interface/ascent.cmi \ kernel/inductive.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ kernel/reduction.cmi contrib/interface/showproof_ct.cmo kernel/sign.cmi \ - lib/stamps.cmi kernel/term.cmi contrib/interface/translate.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi + kernel/term.cmi contrib/interface/translate.cmi pretyping/typing.cmi \ + lib/util.cmi toplevel/vernacinterp.cmi contrib/interface/translate.cmi: contrib/interface/ascent.cmi \ kernel/environ.cmi pretyping/evd.cmi proofs/proof_type.cmi \ kernel/term.cmi @@ -929,15 +928,15 @@ proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \ pretyping/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ pretyping/reductionops.cmi proofs/refiner.cmi kernel/sign.cmi \ - lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/evar_refiner.cmi + pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/evar_refiner.cmi proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ pretyping/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ - lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/evar_refiner.cmi + pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi kernel/names.cmi \ @@ -970,36 +969,36 @@ proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \ pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \ lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi kernel/sign.cmi \ - lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/tacred.cmi kernel/term.cmi parsing/termast.cmi \ pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ proofs/proof_trees.cmi proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \ pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \ lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx kernel/sign.cmx \ - lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/tacred.cmx kernel/term.cmx parsing/termast.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi library/nametab.cmi \ - pretyping/pretyping.cmi lib/stamps.cmi pretyping/tacred.cmi \ - kernel/term.cmi lib/util.cmi proofs/proof_type.cmi + pretyping/pretyping.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi \ + proofs/proof_type.cmi proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx \ pretyping/evd.cmx kernel/names.cmx library/nametab.cmx \ - pretyping/pretyping.cmx lib/stamps.cmx pretyping/tacred.cmx \ - kernel/term.cmx lib/util.cmx proofs/proof_type.cmi + pretyping/pretyping.cmx pretyping/tacred.cmx kernel/term.cmx lib/util.cmx \ + proofs/proof_type.cmi proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ proofs/logic.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - lib/stamps.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi + kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ + proofs/refiner.cmi proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \ proofs/logic.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - lib/stamps.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi + kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ + proofs/refiner.cmi proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ lib/dyn.cmi kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -1027,16 +1026,16 @@ proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \ pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi \ - kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \ + pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ proofs/tacmach.cmi proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx pretyping/instantiate.cmx \ proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx \ - kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/refiner.cmx kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \ + pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/tacmach.cmi proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi @@ -1272,7 +1271,7 @@ tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi library/global.cmi pretyping/indrec.cmi \ kernel/inductive.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \ + kernel/reduction.cmi kernel/sign.cmi proofs/tacinterp.cmi \ proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ pretyping/termops.cmi lib/util.cmi tactics/wcclausenv.cmi \ tactics/tacticals.cmi @@ -1280,7 +1279,7 @@ tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx library/global.cmx pretyping/indrec.cmx \ kernel/inductive.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \ + kernel/reduction.cmx kernel/sign.cmx proofs/tacinterp.cmx \ proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx \ pretyping/termops.cmx lib/util.cmx tactics/wcclausenv.cmx \ tactics/tacticals.cmi @@ -1291,10 +1290,9 @@ tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi \ proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi kernel/sign.cmi lib/stamps.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - tactics/tactics.cmi + pretyping/reductionops.cmi kernel/sign.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ @@ -1302,10 +1300,9 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx \ proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx kernel/sign.cmx lib/stamps.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - tactics/tactics.cmi + pretyping/reductionops.cmx kernel/sign.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx tactics/tactics.cmi tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi @@ -2044,22 +2041,20 @@ contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \ kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ - contrib/interface/showproof_ct.cmo kernel/sign.cmi lib/stamps.cmi \ - proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi \ - pretyping/termops.cmi contrib/interface/translate.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - contrib/interface/showproof.cmi + contrib/interface/showproof_ct.cmo kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ + contrib/interface/translate.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi contrib/interface/showproof.cmi contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ proofs/clenv.cmx parsing/coqast.cmx kernel/declarations.cmx \ kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \ kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ - contrib/interface/showproof_ct.cmx kernel/sign.cmx lib/stamps.cmx \ - proofs/tacmach.cmx kernel/term.cmx parsing/termast.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.cmx kernel/sign.cmx proofs/tacmach.cmx \ + kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ + contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx contrib/interface/showproof.cmi contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -70,7 +70,7 @@ CONFIG=config/coq_config.cmo LIBREP=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ - lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \ + lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ lib/predicate.cmo # Rem: Cygwin already uses variable LIB @@ -183,7 +183,7 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ parsing/termast.cmo \ parsing/astterm.cmo \ parsing/egrammar.cmo parsing/esyntax.cmo toplevel/metasyntax.cmo \ - parsing/printer.cmo lib/stamps.cmo pretyping/typing.cmo \ + parsing/printer.cmo pretyping/typing.cmo \ proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ proofs/evar_refiner.cmo proofs/tacmach.cmo toplevel/himsg.cmo \ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \ diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index dd6f0ef17..5bfad2f52 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -6,7 +6,6 @@ open Environ open Evd open Names open Nameops -open Stamps open Term open Termops open Util diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli index 22c3b7c4e..c84642d77 100755 --- a/contrib/interface/showproof.mli +++ b/contrib/interface/showproof.mli @@ -1,7 +1,6 @@ open Environ open Evd open Names -open Stamps open Term open Util open Proof_type diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4ea4c4f50..09e9adbc5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -59,7 +59,7 @@ type 'a clausenv = { env : clbinding Intmap.t; hook : 'a } -type wc = walking_constraints +type wc = named_context sigma let applyHead n c wc = let rec apprec n c cty wc = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b15abb775..5fd0e0c0e 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -12,6 +12,7 @@ open Util open Names open Term +open Sign open Tacmach open Proof_type open Evar_refiner @@ -52,7 +53,7 @@ type 'a clausenv = { * [hook] is the pointer to the current walking context, for * integrating existential vars and metavars. *) -type wc = walking_constraints (* for a better reading of the following *) +type wc = named_context sigma (* for a better reading of the following *) val unify : constr -> tactic val unify_0 : @@ -99,16 +100,16 @@ val clenv_type_of : wc clausenv -> constr -> constr val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv val make_clenv_binding_apply : - walking_constraints -> + named_context sigma -> int -> constr * constr -> (bindOcc * types) list -> - walking_constraints clausenv + named_context sigma clausenv val make_clenv_binding : - walking_constraints -> + named_context sigma -> constr * constr -> (bindOcc * types) list -> - walking_constraints clausenv + named_context sigma clausenv (* Exported for program.ml only *) val clenv_add_sign : diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 45c57eff4..12f928e99 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -10,11 +10,11 @@ open Pp open Util -open Stamps open Names open Term open Environ open Evd +open Sign open Reductionops open Typing open Instantiate @@ -27,21 +27,19 @@ open Refiner 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 walking_constraints = readable_constraints idstamped -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a -type w_tactic = walking_constraints -> walking_constraints +type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a +type w_tactic = named_context sigma -> named_context sigma let local_Constraints gs = refiner Change_evars gs let startWalk gls = let evc = project_with_focus gls in - let wc = (ids_mk evc) in - (wc, + (evc, (fun wc' gls' -> - if not !Options.debug or (ids_eq wc wc' & gls.it = gls'.it) then + 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 (ids_it wc')} + 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')})*) @@ -55,10 +53,10 @@ let walking_THEN wt rt gls = let walking wt = walking_THEN (fun wc -> (wt wc,())) (fun () -> tclIDTAC) let extract_decl sp evc = - let evdmap = (ts_it evc).decls in + let evdmap = evc.sigma in let evd = Evd.map evdmap sp in - (ts_mk { hyps = evd.evar_hyps; - decls = Evd.rmv evdmap sp }) + { it = evd.evar_hyps; + sigma = Evd.rmv evdmap sp } let restore_decl sp evd evc = (rc_add evc (sp,evd)) @@ -74,45 +72,37 @@ let restore_decl sp evd evc = * 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 : walking_constraints) = - let hyps = (ts_it (ids_it wc)).hyps - and evd = Evd.map (ts_it (ids_it wc)).decls sp in - let (wc' : walking_constraints) = ids_mod (extract_decl sp) wc in + (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 ts_eq (ids_it wc') (ids_it wc'') then +(* if not (ids_eq wc wc'') then error "w_saving_focus"; *) + if wc'==wc'' then wt' rslt wc else - let wc''' = ids_mod (restore_decl sp evd) wc'' in - wt' rslt - (ids_mod - (ts_mod (fun evc -> - { hyps = hyps; - decls = evc.decls })) - wc''') + let wc''' = restore_decl sp evd wc'' in + wt' rslt {it = hyps; sigma = wc'''.sigma} -let w_add_sign (id,t) (wc : walking_constraints) = - ids_mk (ts_mod - (fun evr -> - { hyps = Sign.add_named_decl (id,None,t) evr.hyps; - decls = evr.decls }) - (ids_it wc)) +let w_add_sign (id,t) (wc : named_context sigma) = + { it = Sign.add_named_decl (id,None,t) wc.it; + sigma = wc.sigma } let ctxt_type_of evc c = - type_of (Global.env_of_context (ts_it evc).hyps) (ts_it evc).decls c + type_of (Global.env_of_context evc.it) evc.sigma c let w_IDTAC wc = wc let w_Focusing sp wt = w_Focusing_THEN sp (fun wc -> (wt wc,())) (fun _ -> w_IDTAC) -let w_Focus sp wc = ids_mod (extract_decl sp) wc +let w_Focus sp wc = extract_decl sp wc -let w_Underlying wc = (ts_it (ids_it wc)).decls +let w_Underlying wc = wc.sigma let w_whd wc c = Evarutil.whd_castappevar (w_Underlying wc) c -let w_type_of wc c = ctxt_type_of (ids_it wc) c -let w_env wc = get_env (ids_it wc) -let w_hyps wc = named_context (get_env (ids_it wc)) +let w_type_of wc c = ctxt_type_of wc c +let w_env wc = get_env wc +let w_hyps wc = named_context (get_env wc) let w_ORELSE wt1 wt2 wc = try wt1 wc with e when catchable_exception e -> wt2 wc let w_defined_const wc sp = defined_constant (w_env wc) sp @@ -123,17 +113,17 @@ 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 : walking_constraints) = +let w_Declare sp ty (wc : named_context sigma) = let _ = w_type_of wc ty in (* Utile ?? *) - let sign = get_hyps (ids_it wc) in + let sign = get_hyps wc in let newdecl = mk_goal sign ty in - ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints) + ((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 - ctxt_type_of (ids_it (w_Focus sp wc)) (mkCast (c,spdecl.evar_concl)) + ctxt_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl)) with Not_found -> error "Instantiation contains unlegal variables" in @@ -143,7 +133,7 @@ let w_Define sp c wc = evar_concl = spdecl.evar_concl; evar_body = Evar_defined c } in - (ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc) + Proof_trees.rc_add wc (sp,spdecl') | _ -> error "define_evar" @@ -162,7 +152,7 @@ let instantiate_pf n c pfts = error "not so many uninstantiated existential variables" in let wc' = w_Define sp c wc in - let newgc = ts_mk (w_Underlying wc') in + let newgc = w_Underlying wc' in change_constraints_pftreestate newgc pfts let instantiate_pf_com n com pfts = @@ -177,5 +167,5 @@ let instantiate_pf_com n com pfts = in let c = Astterm.interp_constr sigma (Evarutil.evar_env evd) com in let wc' = w_Define sp c wc in - let newgc = ts_mk (w_Underlying wc') in + let newgc = w_Underlying wc' in change_constraints_pftreestate newgc pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 7100e9844..9f09cfba5 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -21,8 +21,8 @@ open Refiner (* Refinement of existential variables. *) -val rc_of_pfsigma : proof_tree sigma -> readable_constraints -val rc_of_glsigma : goal sigma -> readable_constraints +val rc_of_pfsigma : proof_tree sigma -> named_context sigma +val rc_of_glsigma : goal sigma -> named_context sigma (* a [walking_constraints] is a structure associated to a specific goal; it collects all evars of which the goal depends. @@ -32,20 +32,18 @@ val rc_of_glsigma : goal sigma -> readable_constraints hyps : context of the goal; decls : a superset of evars of which the goal may depend })] *) -type walking_constraints - -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a +type 'a result_w_tactic = named_context sigma -> named_context sigma * 'a (* A [w_tactic] is a tactic which modifies the a set of evars of which a goal depend, either by instantiating one, or by declaring a new dependent goal *) -type w_tactic = walking_constraints -> walking_constraints +type w_tactic = named_context sigma -> named_context sigma val local_Constraints : goal sigma -> goal list sigma * validation val startWalk : - goal sigma -> walking_constraints * (walking_constraints -> tactic) + goal sigma -> named_context sigma * (named_context sigma -> tactic) val walking_THEN : 'a result_w_tactic -> ('a -> tactic) -> tactic val walking : w_tactic -> tactic @@ -55,23 +53,23 @@ val w_Focusing_THEN : val w_Declare : evar -> types -> w_tactic val w_Define : evar -> constr -> w_tactic -val w_Underlying : walking_constraints -> evar_map -val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> named_context -val w_whd : walking_constraints -> constr -> constr -val w_type_of : walking_constraints -> constr -> constr -val w_add_sign : (identifier * types) -> walking_constraints - -> walking_constraints +val w_Underlying : named_context sigma -> evar_map +val w_env : named_context sigma -> env +val w_hyps : named_context sigma -> named_context +val w_whd : named_context sigma -> constr -> constr +val w_type_of : named_context sigma -> constr -> constr +val w_add_sign : (identifier * types) -> named_context sigma + -> named_context sigma val w_IDTAC : w_tactic val w_ORELSE : w_tactic -> w_tactic -> w_tactic -val ctxt_type_of : readable_constraints -> constr -> constr -val w_whd_betadeltaiota : walking_constraints -> constr -> constr -val w_hnf_constr : walking_constraints -> constr -> constr -val w_conv_x : walking_constraints -> constr -> constr -> bool -val w_const_value : walking_constraints -> constant -> constr -val w_defined_const : walking_constraints -> constant -> bool -val w_defined_evar : walking_constraints -> existential_key -> bool +val ctxt_type_of : named_context sigma -> constr -> constr +val w_whd_betadeltaiota : named_context sigma -> constr -> constr +val w_hnf_constr : named_context sigma -> constr -> constr +val w_conv_x : named_context sigma -> constr -> constr -> bool +val w_const_value : named_context sigma -> constant -> constr +val w_defined_const : named_context sigma -> constant -> bool +val w_defined_evar : named_context sigma -> existential_key -> bool val instantiate_pf : int -> constr -> pftreestate -> pftreestate val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 429e93aa4..c60abbc28 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -15,7 +15,6 @@ open Term open Termops open Sign open Evd -open Stamps open Environ open Evarutil open Proof_type @@ -69,38 +68,21 @@ let is_tactic_proof pf = (pf.subproof <> None) (* A readable constraint is a global constraint plus a focus set of existential variables and a signature. *) -type evar_recordty = { - hyps : named_context; - decls : evar_map } - -and readable_constraints = evar_recordty timestamped - (* Functions on readable constraints *) let mt_evcty gc = - ts_mk { hyps = empty_named_context; decls = gc } + { it = empty_named_context; sigma = gc } -let evc_of_evds evds gl = - ts_mk { hyps = gl.evar_hyps; decls = evds } +let rc_of_gc evds gl = + { it = gl.evar_hyps; sigma = evds } -let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl - let rc_add evc (k,v) = - ts_mod - (fun evc -> { hyps = evc.hyps; - decls = Evd.add evc.decls k v }) - evc - -let get_hyps evc = (ts_it evc).hyps -let get_env evc = Global.env_of_context (ts_it evc).hyps -let get_decls evc = (ts_it evc).decls -let get_gc evc = (ts_mk (ts_it evc).decls) - -let remap evc (k,v) = - ts_mod - (fun evc -> { hyps = evc.hyps; - decls = Evd.add evc.decls k v }) - evc + { it = evc.it; + sigma = Evd.add evc.sigma k v } + +let get_hyps evc = evc.it +let get_env evc = Global.env_of_context evc.it +let get_gc evc = evc.sigma let pf_lookup_name_as_renamed hyps ccl s = Detyping.lookup_name_as_renamed hyps ccl s @@ -215,13 +197,11 @@ let pr_evd evd = h 0 [< pr_id (id_of_existential ev) ; 'sTR"==" ; pe >]) (Evd.to_list evd) -let pr_decls decls = pr_evd (ts_it decls) +let pr_decls decls = pr_evd decls let pr_evc evc = - let stamp = ts_stamp evc in - let evc = ts_it evc in - let pe = pr_evd evc.decls in - [< 'sTR"#" ; 'iNT stamp ; 'sTR"]=" ; pe >] + let pe = pr_evd evc.sigma in + [< pe >] let pr_evars = prlist_with_sep pr_fnl diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 4ad1509fe..200adac0a 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -10,7 +10,6 @@ (*i*) open Util -open Stamps open Names open Term open Sign @@ -37,19 +36,11 @@ val is_tactic_proof : proof_tree -> bool (*s A readable constraint is a global constraint plus a focus set of existential variables and a signature. *) -type evar_recordty = { - hyps : named_context; - decls : evar_map } - -and readable_constraints = evar_recordty timestamped - -val rc_of_gc : global_constraints -> goal -> readable_constraints -val rc_add : readable_constraints -> int * goal -> readable_constraints -val get_hyps : readable_constraints -> named_context -val get_env : readable_constraints -> env -val get_decls : readable_constraints -> evar_map -val get_gc : readable_constraints -> global_constraints -val remap : readable_constraints -> int * goal -> readable_constraints +val rc_of_gc : evar_map -> goal -> named_context sigma +val rc_add : named_context sigma -> int * goal -> named_context sigma +val get_hyps : named_context sigma -> named_context +val get_env : named_context sigma -> env +val get_gc : named_context sigma -> evar_map val pf_lookup_name_as_renamed : named_context -> constr -> identifier -> int option @@ -67,8 +58,8 @@ val pr_subgoals : goal list -> std_ppcmds val pr_subgoal : int -> goal list -> std_ppcmds val pr_decl : goal -> std_ppcmds -val pr_decls : global_constraints -> std_ppcmds -val pr_evc : readable_constraints -> std_ppcmds +val pr_decls : evar_map -> std_ppcmds +val pr_evc : named_context sigma -> std_ppcmds val prgl : goal -> std_ppcmds val pr_seq : goal -> std_ppcmds diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 81c57e539..9965488c9 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -9,7 +9,6 @@ open Environ open Evd open Names -open Stamps open Term open Util (*i*) @@ -55,14 +54,10 @@ type prim_rule = { params : Coqast.t list; terms : constr list } -(* A global constraint is a mappings of existential variables - with some extra information for the program tactic *) -type global_constraints = evar_map timestamped - (* Signature useful to define the tactic type *) type 'a sigma = { it : 'a ; - sigma : global_constraints } + sigma : evar_map } (*s Proof trees. [ref] = [None] if the goal has still to be proved, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 2c57806b5..aab94e4b4 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -12,7 +12,6 @@ open Environ open Evd open Names -open Stamps open Term open Util (*i*) @@ -58,10 +57,6 @@ type prim_rule = { params : Coqast.t list; terms : constr list } -(* A global constraint is a mappings of existential variables - with some extra information for the program tactic *) -type global_constraints = evar_map timestamped - (* The type [goal sigma] is the type of subgoal. It has the following form \begin{verbatim} it = { evar_concl = [the conclusion of the subgoal] @@ -94,7 +89,7 @@ type global_constraints = evar_map timestamped type ['a] (see below the form of a [goal sigma] *) type 'a sigma = { it : 'a ; - sigma : global_constraints } + sigma : evar_map} (*s Proof trees. [ref] = [None] if the goal has still to be proved, diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e7b2c78f7..4ee7fc5c8 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -10,7 +10,6 @@ open Pp open Util -open Stamps open Term open Termops open Sign @@ -161,7 +160,7 @@ let refiner = function | Prim pr as r -> let prim_fun = prim_refiner pr in (fun goal_sigma -> - let sgl = prim_fun (ts_it goal_sigma.sigma) goal_sigma.it in + let sgl = prim_fun goal_sigma.sigma goal_sigma.it in ({it=sgl; sigma = goal_sigma.sigma}, (fun spfl -> assert (check_subproof_connection sgl spfl); @@ -189,7 +188,7 @@ let refiner = function | Change_evars as r -> (fun goal_sigma -> let gl = goal_sigma.it in - let sgl = [norm_goal (ts_it goal_sigma.sigma) gl] in + let sgl = [norm_goal goal_sigma.sigma gl] in ({it=sgl;sigma=goal_sigma.sigma}, (fun spfl -> assert (check_subproof_connection sgl spfl); @@ -379,10 +378,10 @@ let weak_progress gls ptree = (List.length gls.it <> 1) or (not (same_goal (List.hd gls.it) ptree.it)) - +(* Il y avait ici un ts_eq ........ *) let progress gls ptree = (weak_progress gls ptree) or - (not (ts_eq ptree.sigma gls.sigma)) + (not (ptree.sigma == gls.sigma)) (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves @@ -520,8 +519,8 @@ let tactic_list_tactic tac gls = (* solve_subgoal : - (global_constraints ref * goal list * validation -> - global_constraints ref * goal list * validation) -> + (evar_map ref * goal list * validation -> + evar_map ref * goal list * validation) -> (proof_tree sigma -> proof_tree sigma) solve_subgoal tac pf_sigma applies the tactic tac at the nth subgoal of pf_sigma *) @@ -530,7 +529,7 @@ let solve_subgoal tacl pf_sigma = let gl,p = frontier pf in let r = tacl (sigr,gl,p) in let (sigr,gll,pl) = - if (ts_it !sigr) == (ts_it pf_sigma.sigma) then r + if !sigr == pf_sigma.sigma then r else then_tac norm_evar_tac r in repackage sigr (pl (List.map leaf gll)) @@ -549,13 +548,13 @@ let solve_subgoal tacl pf_sigma = type pftreestate = { tpf : proof_tree ; - tpfsigma : global_constraints; + tpfsigma : evar_map; tstack : (int * validation) list } let proof_of_pftreestate pts = pts.tpf let is_top_pftreestate pts = pts.tstack = [] let cursor_of_pftreestate pts = List.map fst pts.tstack -let evc_of_pftreestate pts = ts_it pts.tpfsigma +let evc_of_pftreestate pts = pts.tpfsigma let top_goal_of_pftreestate pts = { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma } @@ -640,14 +639,14 @@ let weak_undo_pftreestate pts = let mk_pftreestate g = { tpf = leaf g; tstack = []; - tpfsigma = ts_mk Evd.empty } + tpfsigma = Evd.empty } (* Extracts a constr from a proof-tree state ; raises an error if the proof is not complete or the state does not correspond to the head of the proof-tree *) let extract_open_pftreestate pts = - extract_open_proof (ts_it pts.tpfsigma) pts.tpf + extract_open_proof pts.tpfsigma pts.tpf let extract_pftreestate pts = if pts.tstack <> [] then @@ -659,7 +658,7 @@ let extract_pftreestate pts = errorlabstrm "extract_proof" [< 'sTR "Attempt to save an incomplete proof" >]; let env = Global.env_of_context pts.tpf.goal.evar_hyps in - strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm + strong whd_betaiotaevar env pts.tpfsigma pfterm (*** local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm ***) @@ -882,7 +881,7 @@ let tclINFO (tac : tactic) gls = let sign = (sig_it gls).evar_hyps in mSGNL(hOV 0 [< 'sTR" == "; print_subscript - ((compose ts_it sig_sig) gls) sign pf >]) + (sig_sig gls) sign pf >]) with e when catchable_exception e -> mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >]) end; diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 4c9fade3e..385d6e8b1 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -11,6 +11,7 @@ (*i*) open Term open Sign +open Evd open Proof_trees open Proof_type (*i*) @@ -18,14 +19,14 @@ open Proof_type (* The refiner (handles primitive rules and high-level tactics). *) val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> global_constraints +val sig_sig : 'a sigma -> evar_map -val project_with_focus : goal sigma -> readable_constraints +val project_with_focus : goal sigma -> named_context sigma -val unpackage : 'a sigma -> global_constraints ref * 'a -val repackage : global_constraints ref -> 'a -> 'a sigma +val unpackage : 'a sigma -> evar_map ref * 'a +val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : - global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c type transformation_tactic = proof_tree -> (goal list * validation) @@ -117,7 +118,7 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool -val evc_of_pftreestate : pftreestate -> Evd.evar_map +val evc_of_pftreestate : pftreestate -> evar_map val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma @@ -141,7 +142,7 @@ val next_unproven : pftreestate -> pftreestate val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate - : global_constraints -> pftreestate -> pftreestate + : evar_map -> pftreestate -> pftreestate (*s Pretty-printers. *) @@ -150,10 +151,10 @@ val change_constraints_pftreestate open Pp (*i*) -val print_proof : Evd.evar_map -> named_context -> proof_tree -> std_ppcmds +val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expression -> std_ppcmds val print_script : - bool -> Evd.evar_map -> named_context -> proof_tree -> std_ppcmds + bool -> evar_map -> named_context -> proof_tree -> std_ppcmds val print_treescript : - Evd.evar_map -> named_context -> proof_tree -> std_ppcmds + evar_map -> named_context -> proof_tree -> std_ppcmds diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index f4766963f..5e4b6b495 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -9,7 +9,6 @@ (* $Id$ *) open Util -open Stamps open Names open Sign open Term @@ -40,8 +39,7 @@ let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac let sig_it = Refiner.sig_it -let sig_sig = Refiner.sig_sig -let project = compose ts_it sig_sig +let project = Refiner.sig_sig let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps let pf_hyps gls = (sig_it gls).evar_hyps diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6a2ca4414..0a685a447 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -13,6 +13,7 @@ open Names open Term open Sign open Environ +open Evd open Reduction open Proof_trees open Proof_type @@ -27,15 +28,14 @@ type validation = Proof_type.validation;; type tactic = Proof_type.tactic;; val sig_it : 'a sigma -> 'a -val sig_sig : goal sigma -> global_constraints -val project : goal sigma -> Evd.evar_map +val project : goal sigma -> evar_map -val re_sig : 'a -> global_constraints -> 'a sigma +val re_sig : 'a -> evar_map -> 'a sigma -val unpackage : 'a sigma -> global_constraints ref * 'a -val repackage : global_constraints ref -> 'a -> 'a sigma +val unpackage : 'a sigma -> evar_map ref * 'a +val repackage : evar_map ref -> 'a -> 'a sigma val apply_sig_tac : - global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c + evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c val pf_concl : goal sigma -> constr val pf_env : goal sigma -> env @@ -63,7 +63,7 @@ val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr val pf_reduce : - (env -> Evd.evar_map -> constr -> constr) -> + (env -> evar_map -> constr -> constr) -> goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr @@ -94,7 +94,7 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool -val evc_of_pftreestate : pftreestate -> Evd.evar_map +val evc_of_pftreestate : pftreestate -> evar_map val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma val traverse : int -> pftreestate -> pftreestate @@ -113,7 +113,7 @@ val next_unproven : pftreestate -> pftreestate val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate val change_constraints_pftreestate : - global_constraints -> pftreestate -> pftreestate + evar_map -> pftreestate -> pftreestate val instantiate_pf : int -> constr -> pftreestate -> pftreestate val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate @@ -243,7 +243,7 @@ val hide_cbindll_tactic : open Pp (*i*) -val pr_com : Evd.evar_map -> goal -> Coqast.t -> std_ppcmds +val pr_com : evar_map -> goal -> Coqast.t -> std_ppcmds val pr_gls : goal sigma -> std_ppcmds val pr_glls : goal list sigma -> std_ppcmds val pr_tactic : tactic_expression -> std_ppcmds diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b71f7ab2a..70f30187d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -129,7 +129,7 @@ let pf_is_matching gls pat n = is_matching_conv (w_env wc) (w_Underlying wc) pat n let pf_matches gls pat n = - matches_conv (pf_env gls) (Stamps.ts_it (sig_sig gls)) pat n + matches_conv (pf_env gls) (project gls) pat n (* [OnCL clausefinder clausetac] * executes the clausefinder to find the clauses, and then executes the diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 804555583..c9247c09e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -10,7 +10,6 @@ open Pp open Util -open Stamps open Names open Nameops open Sign diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 60d48530c..b91aa09e6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -12,6 +12,7 @@ open Names open Term open Environ +open Sign open Tacmach open Proof_type open Reduction @@ -27,7 +28,7 @@ open Nametab (*s General functions. *) -val type_clenv_binding : walking_constraints -> +val type_clenv_binding : named_context sigma -> constr * constr -> constr substitution -> constr val string_of_inductive : constr -> string diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 0df646c0c..3b93cce07 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -28,7 +28,7 @@ open Evar_refiner write to Eduardo.Gimenez@inria.fr and ask for the prize :-) -- Eduardo (11/8/97) *) -type wc = walking_constraints +type wc = named_context sigma let pf_get_new_id id gls = next_ident_away id (pf_ids_of_hyps gls) diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index cd88cc1b5..24174e508 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -32,7 +32,7 @@ type arg_binder = type arg_bindings = (arg_binder * constr) list -type wc = walking_constraints +type wc = named_context sigma val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv |