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

1 files changed, 33 insertions, 43 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 45c57eff4e..12f928e999 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