Suppression des local_constraints, des ctxtty et du focus.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 62 insertions, 209 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 65307debea..b15abb775f 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -129,5 +129,5 @@ val pr_clenv : 'a clausenv -> Pp.std_ppcmds
 (* [abstract_list_all env sigma t c l]                     *)
 (* abstracts the terms in l over c to get a term of type t *)
 val abstract_list_all :
-  Environ.env -> 'a Evd.evar_map -> constr -> constr -> constr list -> constr
+  Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index a4fb3fe9b2..fe809b6244 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -32,7 +32,7 @@ type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
 type w_tactic = walking_constraints -> walking_constraints
 
 
-let local_Constraints lc gs = refiner (Local_constraints lc) gs
+let local_Constraints lc gs = refiner Change_evars gs
 
 let startWalk gls =
   let evc = project_with_focus gls in
@@ -40,11 +40,11 @@ let startWalk gls =
   (wc,
    (fun wc' gls' ->
       if not !Options.debug or (ids_eq wc wc' & gls.it = gls'.it) then
-        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then
+(*        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*)
           tclIDTAC {it=gls'.it; sigma = get_gc (ids_it wc')}
-        else
+(*        else
           (local_Constraints (get_focus (ids_it wc'))
-             {it=gls'.it; sigma = get_gc (ids_it wc')})
+             {it=gls'.it; sigma = get_gc (ids_it wc')})*)
       else error "Walking"))
 
 let walking_THEN wt rt gls =
@@ -58,17 +58,10 @@ let extract_decl sp evc =
   let evdmap = (ts_it evc).decls in
   let evd = Evd.map evdmap sp in 
   (ts_mk { hyps = evd.evar_hyps;
-           focus = get_lc evd;
            decls = Evd.rmv evdmap sp })
 
 let restore_decl sp evd evc =
-  let newctxt = { lc = (ts_it evc).focus;
-                  pgm = (get_pgm evd) } in
-  let newgoal = { evar_hyps = evd.evar_hyps; 
-		  evar_concl = evd.evar_concl;
-		  evar_body = evd.evar_body;
-                  evar_info = Some newctxt } in
-  (rc_add evc (sp,newgoal))
+  (rc_add evc (sp,evd))
 
 
 (* [w_Focusing sp wt wc]
@@ -82,8 +75,7 @@ let restore_decl sp evd evc =
 
 let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
                        (wc : walking_constraints) =
-  let focus = (ts_it (ids_it wc)).focus
-  and hyps  = (ts_it (ids_it wc)).hyps
+  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
   let (wc'',rslt) = wt wc' in 
@@ -96,15 +88,13 @@ let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
       (ids_mod
          (ts_mod (fun evc ->
                     { hyps = hyps;
-                      focus = focus;
                       decls = evc.decls }))
          wc''')
       
 let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
-               { focus = evr.focus;
-		 hyps = Sign.add_named_decl (id,None,t) evr.hyps;
+	       { hyps = Sign.add_named_decl (id,None,t) evr.hyps;
 		 decls = evr.decls })
             (ids_it wc))
 
@@ -135,25 +125,10 @@ 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_type_of wc ty in (* Utile ?? *)
-  let access  = get_focus (ids_it wc)
-  and sign = get_hyps (ids_it wc) in
-  let newdecl = mk_goal (mt_ctxt access) sign ty in 
+  let sign = get_hyps (ids_it wc) in
+  let newdecl = mk_goal sign ty in 
   ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints)
 
-let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
-
-let evars_of sigma constr = 
-  let rec filtrec acc c =
-    match kind_of_term c with
-    | Evar (ev, cl) ->
-	if Evd.in_dom (ts_it sigma).decls ev then
-	  Intset.add ev (Array.fold_left filtrec acc cl)
-	else
-	  Array.fold_left filtrec acc cl
-    | _ -> fold_constr filtrec acc c
-  in 
-  filtrec Intset.empty constr
-
 let w_Define sp c wc =
   let spdecl = Evd.map (w_Underlying wc) sp in
   let cty = 
@@ -164,10 +139,8 @@ let w_Define sp c wc =
   in 
   match spdecl.evar_body with
     | Evar_empty ->
-    	let access = evars_of (ids_it wc) c in
     	let spdecl' = { evar_hyps = spdecl.evar_hyps;
                        	evar_concl = spdecl.evar_concl;
-                       	evar_info = Some (mt_ctxt access);
                        	evar_body = Evar_defined c }
     	in 
 	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 88071b3af2..13a4a5e410 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -53,7 +53,6 @@ val w_Focusing_THEN :
   evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
 
 val w_Declare    : evar -> types -> w_tactic
-val w_Declare_At : evar -> evar -> types -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> enamed_declarations
@@ -74,7 +73,5 @@ 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 evars_of     : readable_constraints -> constr -> local_constraints
-
 val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ed13b9c253..cdb45ccedc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -96,8 +96,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | Meta _ ->
 	if occur_meta conclty then
           raise (RefinerError (OccurMetaGoal conclty));
-	let ctxt = out_some goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota conclty))::goalacc, conclty
+	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,ty) ->
 	let _ = type_of env sigma ty in
@@ -136,8 +135,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
-	let ctxt = out_some goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota ty))::goalacc,ty
+	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
 
     | App (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
@@ -373,7 +371,6 @@ let prim_refiner r sigma goal =
   let env = evar_env goal in
   let sign = goal.evar_hyps in
   let cl = goal.evar_concl in
-  let info = out_some goal.evar_info in
   match r with
     | { name = Intro; newids = [id] } ->
     	if !check && mem_named_context id sign then
@@ -381,13 +378,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sg = mk_goal info (add_named_decl (id,None,c1) sign)
+	       let sg = mk_goal (add_named_decl (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
 	       [sg]
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
-		 mk_goal info (add_named_decl (id,Some c1,t1) sign)
+		 mk_goal (add_named_decl (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -401,12 +398,12 @@ let prim_refiner r sigma goal =
 	   | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,None,c1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sign' = insert_after_hyp sign whereid (id,Some c1,t1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -417,12 +414,12 @@ let prim_refiner r sigma goal =
            | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,None,c1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let sign' = replace_hyp sign id (id,Some c1,t1) in
-	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
+	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -430,8 +427,8 @@ let prim_refiner r sigma goal =
 	
     | { name = Cut b; terms = [t]; newids = [id] } ->
         if occur_meta t then error_use_instantiate();
-        let sg1 = mk_goal info sign (nf_betaiota t) in
-        let sg2 = mk_goal info (add_named_decl (id,None,t) sign) cl in
+        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in
         if b then [sg1;sg2] else [sg2;sg1]  
 
     | { name = FixRule; hypspecs = []; terms = []; 
@@ -451,7 +448,7 @@ let prim_refiner r sigma goal =
      	check_ind n cl;
 	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
-        let sg = mk_goal info (add_named_decl (f,None,cl) sign) cl in
+        let sg = mk_goal (add_named_decl (f,None,cl) sign) cl in
         [sg]
     
     | { name = FixRule; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -479,7 +476,7 @@ let prim_refiner r sigma goal =
 		error "name already used in the environment";
 	      mk_sign (add_named_decl (f,None,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mk_goal info sign) (cl::lar)
+	      List.map (mk_goal sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
@@ -505,7 +502,7 @@ let prim_refiner r sigma goal =
               with
               |	Not_found ->
                   mk_sign (add_named_decl (f,None,ar) sign) (lar',lf'))
-	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
+	  | ([],[]) -> List.map (mk_goal sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
 	mk_sign sign (cl::lar,lf)
@@ -520,19 +517,19 @@ let prim_refiner r sigma goal =
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info sign cl' in
+          let sg = mk_goal sign cl' in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
 
     | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
-	[mk_goal info (convert_hyp sign sigma id ty) cl]
+	[mk_goal (convert_hyp sign sigma id ty) cl]
 
     | { name = Convert_defbody; hypspecs = [id]; terms = [c] } ->
-	[mk_goal info (convert_def true sign sigma id c) cl]
+	[mk_goal (convert_def true sign sigma id c) cl]
 
     | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
-	[mk_goal info (convert_def false sign sigma id ty) cl]
+	[mk_goal (convert_def false sign sigma id ty) cl]
 
     | { name = Thin; hypspecs = ids } ->
 	let clear_aux sign id =
@@ -541,7 +538,7 @@ let prim_refiner r sigma goal =
           remove_hyp sign id 
 	in
 	let sign' = List.fold_left clear_aux sign ids in
-     	let sg = mk_goal info sign' cl in
+     	let sg = mk_goal sign' cl in
      	[sg]
 
     | { name = ThinBody; hypspecs = ids } ->
@@ -551,7 +548,7 @@ let prim_refiner r sigma goal =
           env'
 	in
 	let sign' = named_context (List.fold_left clear_aux env ids) in
-     	let sg = mk_goal info sign' cl in
+     	let sg = mk_goal sign' cl in
      	[sg]
 
     | { name = Move withdep; hypspecs = ids } ->
@@ -560,7 +557,7 @@ let prim_refiner r sigma goal =
   	let (left,right,declfrom,toleft) = split_sign hfrom hto sign in
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
-  	[mk_goal info hyps' cl]
+  	[mk_goal hyps' cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 3c960b657d..ba1ca70318 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -34,7 +34,7 @@ val without_check : tactic -> tactic
 
 (* The primitive refiner. *)
 
-val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list
 
 val prim_extractor :
   (identifier list -> proof_tree -> constr)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 5d015dbf83..f6424df8dc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -204,7 +204,7 @@ let delete_all_proofs = init_proofs
 (*********************************************************************)
 
 let start_proof na str sign concl =
-  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
+  let top_goal = mk_goal sign concl in
   let ts = { 
     top_hyps = (sign,empty_named_context);
     top_goal = top_goal;
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 3003f20c6c..c6a1df1d92 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -27,27 +27,11 @@ let is_bind = function
   | Bindings _ -> true
   | _ -> false
 
-let lc_toList lc = Intset.elements lc
-
 (* Functions on goals *)
 
-let mk_goal ctxt hyps cl = 
+let mk_goal hyps cl = 
   { evar_hyps = hyps; evar_concl = cl; 
-    evar_body = Evar_empty; evar_info = Some ctxt }
-
-(* Functions on the information associated with existential variables  *)
-
-let mt_ctxt lc = { pgm = None; lc = lc }
-
-let get_ctxt gl = out_some gl.evar_info
-
-let get_pgm gl = (out_some gl.evar_info).pgm
-
-let set_pgm pgm ctxt = { ctxt with pgm = pgm }
-
-let get_lc gl = (out_some gl.evar_info).lc
-
-let set_lc lc ctxt = { ctxt with lc = lc }
+    evar_body = Evar_empty}
 
 (* Functions on proof trees *)
 
@@ -96,7 +80,6 @@ type global_constraints  = enamed_declarations timestamped
    of existential variables and a signature. *)
 
 type evar_recordty = {
-  focus : local_constraints;
   hyps  : named_context;
   decls : enamed_declarations }
 
@@ -104,63 +87,31 @@ and readable_constraints = evar_recordty timestamped
 
 (* Functions on readable constraints *)
 			     
-let mt_evcty lc gc = 
-  ts_mk { focus = lc; hyps = empty_named_context; decls = gc }
+let mt_evcty gc = 
+  ts_mk { hyps = empty_named_context; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); hyps = gl.evar_hyps; decls = evds }
+  ts_mk { hyps = gl.evar_hyps; decls = evds }
 
 let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
 		       
 let rc_add evc (k,v) = 
   ts_mod
-    (fun evc -> { focus = (Intset.add k evc.focus);
-                  hyps  = evc.hyps;
+    (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_focus evc = (ts_it evc).focus
 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 -> { focus = evc.focus;
-                  hyps  = evc.hyps;
+    (fun evc -> { hyps  = evc.hyps;
                   decls = Evd.add evc.decls k v })
     evc
 
-let lc_exists f lc = Intset.fold (fun e b -> (f e) or b) lc false
-
-(* [mentions sigma sp loc] is true exactly when [loc] is defined, and [sp] is
- * on [loc]'s access list, or an evar on [loc]'s access list mentions [sp]. *)
-
-let rec mentions sigma sp loc =
-  let loc_evd = Evd.map (ts_it sigma).decls loc in 
-  match loc_evd.evar_body with 
-    | Evar_defined _ -> (Intset.mem sp (get_lc loc_evd) 
-			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
-    | _ -> false
-
-(* ACCESSIBLE SIGMA SP LOC is true exactly when SP is on LOC's access list,
- * or there exists a LOC' on LOC's access list such that
- * MENTIONS SIGMA SP LOC' is true. *)
-
-let rec accessible sigma sp loc =
-  let loc_evd = Evd.map (ts_it sigma).decls loc in 
-  lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)
-
-
-(* [ctxt_access sigma sp] is true when SIGMA is accessing a current
- * accessibility list ACCL, and SP is either on ACCL, or is mentioned
- * in the body of one of the ACCL. *)
-
-let ctxt_access sigma sp =
-  lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus
-
-
 let pf_lookup_name_as_renamed hyps ccl s =
   Detyping.lookup_name_as_renamed hyps ccl s
 
@@ -235,41 +186,27 @@ let pr_subgoal n =
   in 
   prrec n
 
-let pr_pgm ctxt = match ctxt.pgm with
-  | None -> [< >]
-  | Some pgm -> let ppgm = fprterm pgm in [< 'sTR"Realizer " ; ppgm >]
-					    
-let pr_ctxt ctxt =
-  let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >]
-
 let pr_seq evd = 
   let env = evar_env evd
   and cl = evd.evar_concl
-  and info = match evd.evar_info with 
-    | Some i -> i 
-    | None -> anomaly "pr_seq : info = None"
   in
-  let pc = pr_ctxt info in
   let pdcl = pr_named_context_of env in
   let pcl = prterm_env_at_top env cl in
-  hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
+  hOV 0 [< pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
 
 let prgl gl =
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let pgl = pr_seq gl in
-  [< 'sTR"[[" ; plc; 'sTR"]" ; pgl ; 'sTR"]" ; 'sPC >]
+  [< 'sTR"[" ; pgl ; 'sTR"]" ; 'sPC >]
 
 let pr_evgl gl =
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[[" ; plc; 'sTR"] " ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hOV 0 [< 'sTR"[" ; phyps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 let pr_evgl_sign gl = 
-  let plc = pr_idl (List.map id_of_existential (lc_toList (get_lc gl))) in
   let ps = pr_named_context_of (evar_env gl) in
   let pc = prterm gl.evar_concl in
-  hOV 0 [< 'sTR"[[" ; plc ; 'sTR"] " ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
+  hOV 0 [< 'sTR"[" ; ps; 'sPC; 'sTR"|- " ; pc; 'sTR"]" >]
 
 (*  evd.evgoal.lc seems to be printed twice *)
 let pr_decl evd =
@@ -290,13 +227,11 @@ let pr_evd evd =
     
 let pr_decls decls = pr_evd (ts_it decls)
 		       
-let pr_focus accl = pr_idl (List.map id_of_existential (lc_toList accl))
-
 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"[" ; pr_focus evc.focus ; 'sTR"]=" ; pe >]
+  [< 'sTR"#" ; 'iNT stamp ; 'sTR"]=" ; pe >]
 
 let pr_evars = 
   prlist_with_sep pr_fnl
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index d579190b38..00f51fcca0 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -22,14 +22,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : ctxtty -> named_context -> constr -> goal
-
-val mt_ctxt    : local_constraints -> ctxtty
-val get_ctxt   : goal -> ctxtty
-val get_pgm    : goal -> constr option
-val set_pgm    : constr option -> ctxtty -> ctxtty
-val get_lc     : goal -> local_constraints
-val set_lc     : local_constraints -> ctxtty -> ctxtty
+val mk_goal : named_context -> constr -> goal
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
@@ -51,7 +44,6 @@ type global_constraints = enamed_declarations timestamped
     of existential variables and a signature. *)
 
 type evar_recordty = {
-  focus : local_constraints;
   hyps  : named_context;
   decls : enamed_declarations }
 
@@ -61,11 +53,9 @@ 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_focus : readable_constraints -> local_constraints
 val get_decls : readable_constraints -> enamed_declarations
 val get_gc    : readable_constraints -> global_constraints
 val remap     : readable_constraints -> int * goal -> readable_constraints
-val ctxt_access : readable_constraints -> int -> bool
 
 val pf_lookup_name_as_renamed : 
   named_context -> constr -> identifier -> int option
@@ -88,8 +78,6 @@ val pr_evc       : readable_constraints -> std_ppcmds
 
 val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
-val pr_focus     : local_constraints -> std_ppcmds
-val pr_ctxt      : ctxtty -> std_ppcmds
 val pr_evars     : (int * goal) list -> std_ppcmds
 val pr_evars_int : int -> (int * goal) list -> std_ppcmds
 val pr_subgoals_existential : enamed_declarations -> goal list -> std_ppcmds
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 1109a5837d..c866d85ed5 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -57,11 +57,7 @@ type prim_rule = {
 
 type local_constraints = Intset.t
 
-type ctxtty = {
-  pgm    : constr option;
-  lc     : local_constraints } 
-
-type enamed_declarations = ctxtty evar_map
+type enamed_declarations = evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
@@ -88,10 +84,9 @@ type proof_tree = {
 and rule =
   | Prim of prim_rule
   | Tactic of tactic_expression
-  | Context of ctxtty
-  | Local_constraints of local_constraints
+  | Change_evars
 
-and goal = ctxtty evar_info
+and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index bf7162aa3a..3d972da3f9 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -60,11 +60,7 @@ type prim_rule = {
 
 type local_constraints = Intset.t
 
-type ctxtty = {
-  pgm    : constr option;
-  lc     : local_constraints } 
-
-type enamed_declarations = ctxtty evar_map
+type enamed_declarations = evar_map
 
 (* A global constraint is a mappings of existential variables
    with some extra information for the program tactic *)
@@ -120,10 +116,9 @@ type proof_tree = {
 and rule =
   | Prim of prim_rule
   | Tactic of tactic_expression
-  | Context of ctxtty
-  | Local_constraints of local_constraints
+  | Change_evars
 
-and goal = ctxtty evar_info
+and goal = evar_info
 
 and tactic = goal sigma -> (goal list sigma * validation)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 820c6eaff6..921238d459 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -58,8 +58,7 @@ let norm_goal sigma gl =
       (fun (d,b,ty) sign ->
         add_named_decl (d, option_app red_fun b, red_fun ty) sign)
       empty_named_context gl.evar_hyps;
-    evar_body = gl.evar_body;
-    evar_info = gl.evar_info }
+    evar_body = gl.evar_body}
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -184,27 +183,13 @@ let refiner = function
               subproof = Some hidden_proof;
               ref = Some(r,spfl) }))
       
-  | (Context ctxt) as r ->
-      (fun goal_sigma ->
-         let gl = goal_sigma.it in
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
-         ({it=[sg];sigma=goal_sigma.sigma},
-          (fun spfl -> 
-	     assert (check_subproof_connection [sg] spfl);
-             { status = (List.hd spfl).status;
-               goal = gl;
-               subproof = None;
-               ref = Some(r,spfl) })))
-
    (* [Local_constraints lc] makes the local constraints be [lc] and
       normalizes evars *)
 
-  | (Local_constraints lc) as r ->
+  | Change_evars as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
-         let ctxt = set_lc lc (out_some gl.evar_info) in 
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
-	 let sgl = [norm_goal (ts_it goal_sigma.sigma) sg] in
+	 let sgl = [norm_goal (ts_it goal_sigma.sigma) gl] in
 	 ({it=sgl;sigma=goal_sigma.sigma},
           (fun spfl -> 
 	    assert (check_subproof_connection sgl spfl);
@@ -213,9 +198,8 @@ let refiner = function
                subproof = None;
                ref = Some(r,spfl) })))
 
-let context ctxt = refiner (Context ctxt)
 let vernac_tactic texp = refiner (Tactic texp)
-let norm_evar_tac gl = refiner (Local_constraints (get_lc gl.it)) gl
+let norm_evar_tac gl = refiner Change_evars gl
 
 (* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
@@ -241,9 +225,7 @@ let extract_open_proof sigma pf =
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
 	  
-    | {ref=Some(Context ctxt,[pf])} -> (proof_extractor vl) pf
-	  
-    | {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
+    | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
 	  
     | {ref=None;goal=goal} ->
 	let visible_rels =
@@ -390,8 +372,7 @@ let rec tclTHENLIST = function
 (* various progress criterions *)
 let same_goal gl subgoal = 
   (hypotheses subgoal) = (hypotheses gl) &
-  eq_constr (conclusion subgoal) (conclusion gl) &
-  (subgoal.evar_info = gl.evar_info)
+  eq_constr (conclusion subgoal) (conclusion gl)
 
 
 let weak_progress gls ptree =
@@ -801,8 +782,7 @@ let pr_tactic (s,l) =
 let pr_rule = function
   | Prim r -> pr_prim_rule r
   | Tactic texp -> hOV 0 (pr_tactic texp)
-  | Context ctxt -> pr_ctxt ctxt
-  | Local_constraints lc ->
+  | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level *)
       (* [< 'sTR"Local constraint change" >] *)
       (* Use Idtac instead *)
@@ -823,15 +803,15 @@ let thin_sign osign sign =
 
 let rec print_proof sigma osign pf =
   let {evar_hyps=hyps; evar_concl=cl; 
-       evar_info=info; evar_body=body} = pf.goal in
+       evar_body=body} = pf.goal in
   let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
 	hOV 0 [< pr_seq {evar_hyps=hyps'; evar_concl=cl;
-			 evar_info=info; evar_body=body} >]
+			 evar_body=body} >]
     | Some(r,spfl) ->
     	hOV 0 [< hOV 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl;
-				evar_info=info; evar_body=body});
+				evar_body=body});
 		 'sPC ; 'sTR" BY ";
 		 hOV 0 [< pr_rule r >]; 'fNL ;
 		 'sTR"  ";
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index dd85f004ae..290c7debcc 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -34,7 +34,6 @@ val overwriting_add_tactic : string -> (tactic_arg list -> tactic) -> unit
 val lookup_tactic          : string -> (tactic_arg list) -> tactic
 
 val refiner : rule -> tactic
-val context : ctxtty -> tactic
 val vernac_tactic : tactic_expression -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e5ccf6d326..f4766963f9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -71,8 +71,6 @@ let pf_get_hyp_typ gls id =
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
-let pf_ctxt gls      = get_ctxt (sig_it gls)
-
 let pf_interp_constr gls c =
   let evc = project gls in 
   Astterm.interp_constr evc (pf_env gls) c
@@ -287,7 +285,6 @@ let rename_bound_var_goal gls =
 (***************************************)
 
 let vernac_tactic = vernac_tactic
-let context       = context
 
 let add_tactic = Refiner.add_tactic
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index c81748a283..48dcb23689 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -45,7 +45,6 @@ val pf_hyps_types         : goal sigma -> (identifier * constr) list
 val pf_nth_hyp_id         : goal sigma -> int -> identifier
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> identifier list
-val pf_ctxt               : goal sigma -> ctxtty
 val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> constr
@@ -151,8 +150,6 @@ val tclINFO          : tactic -> tactic
 
 val unTAC         : tactic -> goal sigma -> proof_tree sigma
 val vernac_tactic : tactic_expression -> tactic
-val context       : ctxtty -> tactic
-
 
 (*s The most primitive tactics. *)
 
@@ -246,7 +243,7 @@ val hide_cbindll_tactic :
 open Pp
 (*i*)
 
-val pr_com    : 'a Evd.evar_map -> goal -> Coqast.t -> std_ppcmds
+val pr_com    : Evd.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