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

12 files changed, 115 insertions, 167 deletions

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