correction Abstract (et make world passe!)

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

8 files changed, 134 insertions, 124 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 7a9dbb177..5d71e4e6d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -52,14 +52,14 @@ let walking wt = walking_THEN (fun wc -> (wt wc,())) (fun () -> tclIDTAC)
 let extract_decl sp evc =
   let evdmap = (ts_it evc).decls in
   let evd = Evd.map evdmap sp in 
-  (ts_mk { env = evd.evar_env;
+  (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_env = evd.evar_env; 
+  let newgoal = { evar_hyps = evd.evar_hyps; 
 		  evar_concl = evd.evar_concl;
 		  evar_body = evd.evar_body;
                   evar_info = Some newctxt } in
@@ -78,7 +78,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 env  = (ts_it (ids_it wc)).env
+  and 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 
@@ -90,7 +90,7 @@ let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic)
     wt' rslt
       (ids_mod
          (ts_mod (fun evc ->
-                    { env = env;
+                    { hyps = hyps;
                       focus = focus;
                       decls = evc.decls }))
          wc''')
@@ -99,11 +99,12 @@ let w_add_sign (id,t) (wc : walking_constraints) =
   ids_mk (ts_mod
             (fun evr ->
                { focus = evr.focus;
-		 env = push_named_assum (id,t) evr.env;
+		 hyps = Sign.add_named_assum (id,t) evr.hyps;
 		 decls = evr.decls })
             (ids_it wc))
 
-let ctxt_type_of evc c = type_of (ts_it evc).env (ts_it evc).decls c
+let ctxt_type_of evc c = 
+  type_of (Global.env_of_context (ts_it evc).hyps) (ts_it evc).decls c
 
 let w_IDTAC wc = wc
 
@@ -123,8 +124,8 @@ let w_Declare sp (ty,s) (wc : walking_constraints) =
   let c = mkCast (ty,s) in
   let _ = w_type_of wc c in
   let access  = get_focus (ids_it wc)
-  and env = get_env (ids_it wc)in
-  let newdecl = mk_goal (mt_ctxt access) env c in 
+  and sign = get_hyps (ids_it wc) in
+  let newdecl = mk_goal (mt_ctxt access) sign c 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)
@@ -153,7 +154,7 @@ let w_Define sp c wc =
   match spdecl.evar_body with
     | Evar_empty ->
     	let access = evars_of (ids_it wc) c in
-    	let spdecl' = { evar_env = spdecl.evar_env;
+    	let spdecl' = { evar_hyps = spdecl.evar_hyps;
                        	evar_concl = spdecl.evar_concl;
                        	evar_info = Some (mt_ctxt access);
                        	evar_body = Evar_defined c }
@@ -189,7 +190,7 @@ let instantiate_pf_com n com pfts =
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
-  let c = Astterm.interp_constr sigma evd.evar_env com 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
   change_constraints_pftreestate newgc pfts
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 17eff5195..0e7b5dc53 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -18,6 +18,7 @@ open Type_errors
 open Coqast
 open Declare
 open Retyping
+open Evarutil
 
 type refiner_error =
   | BadType of constr * constr * constr
@@ -55,13 +56,14 @@ let conv_leq_goal env sigma arg ty conclty =
     raise (RefinerError (BadType (arg,ty,conclty)))
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
-  let env = goal.evar_env in
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
   match kind_of_term trm with
     | IsMeta mv ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
 	let ctxt = out_some goal.evar_info in 
-	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
+	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | IsCast (t,ty) ->
 	let _ = type_of env sigma ty in
@@ -95,12 +97,13 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
  * Metas should be casted. *)
 
 and mk_hdgoals sigma goal goalacc trm =
-  let env = goal.evar_env in
+  let env = evar_env goal in
+  let hyps = goal.evar_hyps in
   match kind_of_term trm with
     | IsCast (c,ty) when isMeta c ->
 	let _ = type_of env sigma ty in
 	let ctxt = out_some goal.evar_info in  
-	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
+	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
 
     | IsApp (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
@@ -120,7 +123,7 @@ and mk_hdgoals sigma goal goalacc trm =
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
   | harg::tlargs as allargs ->
-      let t = whd_betadeltaiota goal.evar_env sigma funty in
+      let t = whd_betadeltaiota (evar_env goal) sigma funty in
       match kind_of_term t with
 	| IsProd (_,c1,b) ->
 	    let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
@@ -130,7 +133,7 @@ and mk_arggoals sigma goal goalacc funty = function
 	| _ -> raise (RefinerError (CannotApply (t,harg)))
 
 and mk_casegoals sigma goal goalacc p c =
-  let env = goal.evar_env in
+  let env = evar_env goal in
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
@@ -219,24 +222,27 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   else 
     List.rev_append left (moverec [] [declfrom] right)
 
-let apply_to_hyp env id f =
+let apply_to_hyp sign id f =
   let found = ref false in
-  let env' =
-    process_named_context_both_sides
-      (fun env (idc,c,ct as d) tail ->
-	 if idc = id then (found:=true; f env d tail) else push_named_decl d env)
-      env in
-  if (not !check) || !found then env'
-  else error "No such assumption"
+  let sign' =
+    fold_named_context_both_sides
+      (fun sign (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f sign d tail
+	 end else 
+	   add_named_decl d sign)
+      sign empty_named_context
+  in
+  if (not !check) || !found then sign' else error "No such assumption"
 
 let global_vars_set_of_var = function
   | (_,None,t) -> global_vars_set (body_of_type t)
   | (_,Some c,t) ->
       Idset.union (global_vars_set (body_of_type t)) (global_vars_set c)
 
-let check_backward_dependencies env d =
+let check_backward_dependencies sign d =
   if not (Idset.for_all
-	    (fun id -> mem_named_context id (named_context env))
+	    (fun id -> mem_named_context id sign)
 	    (global_vars_set_of_var d))
   then
     error "Can't introduce at that location: free variable conflict"
@@ -249,26 +255,27 @@ let check_forward_dependencies id tail =
 		^ (string_of_id id')))
     tail
 
-let convert_hyp env sigma id ty =
-  apply_to_hyp env id
-    (fun env (idc,c,ct) _ ->
+let convert_hyp sign sigma id ty =
+  apply_to_hyp sign id
+    (fun sign (idc,c,ct) _ ->
+       let env = Global.env_of_context sign in
        if !check && not (is_conv env sigma ty (body_of_type ct)) then
 	 error "convert-hyp rule passed non-converting term";
-       push_named_decl (idc,c,ty) env)
+       add_named_decl (idc,c,ty) sign)
 
-let replace_hyp env id d =
-  apply_to_hyp env id
-    (fun env _ tail ->
+let replace_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign _ tail ->
        if !check then
-	 (check_backward_dependencies env d;
+	 (check_backward_dependencies sign d;
 	  check_forward_dependencies id tail);
-       push_named_decl d env)
+       add_named_decl d sign)
 
-let insert_after_hyp env id d =
-  apply_to_hyp env id
-    (fun env d' _ ->
-       if !check then check_backward_dependencies env d;
-       push_named_decl d (push_named_decl d' env))
+let insert_after_hyp sign id d =
+  apply_to_hyp sign id
+    (fun sign d' _ ->
+       if !check then check_backward_dependencies sign d;
+       add_named_decl d (add_named_decl d' sign))
 
 let remove_hyp env id =
   apply_to_hyp env id
@@ -279,8 +286,8 @@ let remove_hyp env id =
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
-  let env = goal.evar_env in
-  let sign = named_context env in
+  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
@@ -290,13 +297,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sg = mk_goal info (push_named_assum (id,c1) env)
+	       let sg = mk_goal info (add_named_assum (id,c1) sign)
 			  (subst1 (mkVar id) b) in
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
-		 mk_goal info (push_named_def (id,c1,t1) env)
+		 mk_goal info (add_named_def (id,c1,t1) sign)
 		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
@@ -309,13 +316,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let env' = insert_after_hyp env whereid (id,None,c1) in
-	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
+	       let sign' = insert_after_hyp sign whereid (id,None,c1) in
+	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
-	       let env' = insert_after_hyp env whereid (id,Some c1,t1) in
-	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
+	       let sign' = insert_after_hyp sign whereid (id,Some c1,t1) in
+	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -325,13 +332,13 @@ let prim_refiner r sigma goal =
 	(match kind_of_term (strip_outer_cast cl) with
            | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let env' = replace_hyp env id (id,None,c1) in
-	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
+	       let sign' = replace_hyp sign id (id,None,c1) in
+	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
 	       [sg]
            | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let env' = replace_hyp env id (id,Some c1,t1) in
-	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
+	       let sign' = replace_hyp sign id (id,Some c1,t1) in
+	       let sg = mk_goal info sign' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -354,7 +361,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 (push_named_assum (f,cl) env) cl in
+        let sg = mk_goal info (add_named_assum (f,cl) sign) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -382,7 +389,7 @@ let prim_refiner r sigma goal =
 		error "name already used in the environment";
 	      mk_sign (add_named_assum (f,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mk_goal info env) (cl::lar)
+	      List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
@@ -400,17 +407,17 @@ let prim_refiner r sigma goal =
 			  "in coinductive types")
 	in
      	List.iter check_is_coind (cl::lar);
-        let rec mk_env env = function 
+        let rec mk_sign sign = function 
           | (ar::lar'),(f::lf') ->
 	      (try
-                (let _ = lookup_named f env in
+                (let _ = lookup_id f sign in
                 error "name already used in the environment")
               with
-              |	Not_found -> mk_env (push_named_assum (f,ar) env) (lar',lf'))
-	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
+              |	Not_found -> mk_sign (add_named_assum (f,ar) sign) (lar',lf'))
+	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
-	mk_env env (cl::lar,lf)
+	mk_sign sign (cl::lar,lf)
 
     | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
@@ -421,21 +428,22 @@ 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 env cl' in
+          let sg = mk_goal info 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 env sigma id ty') cl]
+	[mk_goal info (convert_hyp sign sigma id ty') cl]
 
     | { name = Thin; hypspecs = ids } ->
-	let clear_aux env id =
+	let clear_aux sign id =
           if !check && occur_var id cl then
             error ((string_of_id id) ^ " is used in the conclusion.");
-          remove_hyp env id in
-	let env' = List.fold_left clear_aux env ids in
-     	let sg = mk_goal info env' cl in
+          remove_hyp sign id 
+	in
+	let sign' = List.fold_left clear_aux sign ids in
+     	let sg = mk_goal info sign' cl in
      	[sg]
 
     | { name = Move withdep; hypspecs = ids } ->
@@ -444,8 +452,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
-	let env' = change_hyps (fun _ -> hyps') env in
-  	[mk_goal info env' cl]
+  	[mk_goal info hyps' cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index be8446101..753421483 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -23,7 +23,7 @@ open Astterm
 (*********************************************************************)
 
 type proof_topstate = {
-  top_hyps : env * env;
+  top_hyps : named_context * named_context;
   top_goal : goal;
   top_strength : strength }
 
@@ -210,10 +210,10 @@ let delete_all_proofs = init_proofs
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str env concl =
-  let top_goal = mk_goal (mt_ctxt Intset.empty) env concl in
+let start_proof na str sign concl =
+  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
   let ts = { 
-    top_hyps = (env,empty_env);
+    top_hyps = (sign,empty_named_context);
     top_goal = top_goal;
     top_strength = str }
   in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 01df40252..0ea35bea9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ val reset_undo : unit -> unit
 
 (*s [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
 
-val start_proof : identifier -> strength -> env -> constr -> unit
+val start_proof : identifier -> strength -> named_context -> constr -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 54febf40b..0c170ef3d 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,6 +8,7 @@ open Sign
 open Evd
 open Stamps
 open Environ
+open Evarutil
 open Proof_type
 open Typing
 
@@ -19,8 +20,8 @@ let lc_toList lc = Intset.elements lc
 
 (* Functions on goals *)
 
-let mk_goal ctxt env cl = 
-  { evar_env = env; evar_concl = cl; 
+let mk_goal ctxt hyps cl = 
+  { evar_hyps = hyps; evar_concl = cl; 
     evar_body = Evar_empty; evar_info = Some ctxt }
 
 (* Functions on the information associated with existential variables  *)
@@ -83,7 +84,7 @@ type global_constraints  = enamed_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  env   : env;
+  hyps  : named_context;
   decls : enamed_declarations }
 
 and readable_constraints = evar_recordty timestamped
@@ -91,21 +92,22 @@ and readable_constraints = evar_recordty timestamped
 (* Functions on readable constraints *)
 			     
 let mt_evcty lc gc = 
-  ts_mk { focus = lc; env = empty_env; decls = gc }
+  ts_mk { focus = lc; hyps = empty_named_context; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); env = gl.evar_env; decls = evds }
+  ts_mk { focus = (get_lc gl); 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);
-                  env   = evc.env;
+                  hyps  = evc.hyps;
                   decls = Evd.add evc.decls k v })
     evc
 
-let get_env   evc = (ts_it evc).env
+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)
@@ -113,7 +115,7 @@ let get_gc    evc = (ts_mk (ts_it evc).decls)
 let remap evc (k,v) = 
   ts_mod
     (fun evc -> { focus = evc.focus;
-                  env   = evc.env;
+                  hyps  = evc.hyps;
                   decls = Evd.add evc.decls k v })
     evc
 
@@ -174,15 +176,17 @@ let pf_lookup_index_as_renamed ccl n =
 let pr_idl idl = prlist_with_sep pr_spc print_id idl
 
 let pr_goal g =
-  let penv = pr_context_of g.evar_env in
-  let pc = prterm_env_at_top g.evar_env g.evar_concl in
+  let env = evar_env g in
+  let penv = pr_context_of env in
+  let pc = prterm_env_at_top env g.evar_concl in
   [< 'sTR"  "; hV 0 [< penv; 'fNL;
 		       'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
                        'sTR "============================"; 'fNL ;
                        'sTR" " ; pc>]; 'fNL>]
 
 let pr_concl n g =
-  let pc = prterm_env_at_top g.evar_env g.evar_concl in
+  let env = evar_env g in
+  let pc = prterm_env_at_top env g.evar_concl in
   [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
      'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]
 
@@ -226,7 +230,7 @@ let pr_ctxt ctxt =
   let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >]
 
 let pr_seq evd = 
-  let env = evd.evar_env
+  let env = evar_env evd
   and cl = evd.evar_concl
   and info = match evd.evar_info with 
     | Some i -> i 
@@ -244,13 +248,13 @@ let prgl gl =
 
 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 (named_context gl.evar_env)) 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"]" >]
 
 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 gl.evar_env 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"]" >]
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 56ef12fb0..9730652f5 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -15,7 +15,7 @@ open Proof_type
 (* This module declares readable constraints, and a few utilities on
    constraints and proof trees *)
 
-val mk_goal : ctxtty -> env -> constr -> goal
+val mk_goal : ctxtty -> named_context -> constr -> goal
 
 val mt_ctxt    : local_constraints -> ctxtty
 val get_ctxt   : goal -> ctxtty
@@ -44,13 +44,14 @@ type global_constraints = enamed_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  env   : env;
+  hyps  : named_context;
   decls : enamed_declarations }
 
 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_focus : readable_constraints -> local_constraints
 val get_decls : readable_constraints -> enamed_declarations
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 1942b4264..53304fe37 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,6 +7,7 @@ open Stamps
 open Term
 open Sign
 open Evd
+open Sign
 open Environ
 open Reduction
 open Instantiate
@@ -17,7 +18,7 @@ open Logic
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
-let hypotheses gl = gl.evar_env
+let hypotheses gl = gl.evar_hyps
 let conclusion gl = gl.evar_concl
 
 let sig_it x = x.it
@@ -43,7 +44,7 @@ let norm_goal sigma gl =
   let red_fun = nf_ise1 sigma in
   let ncl = red_fun gl.evar_concl in
   { evar_concl = ncl;
-    evar_env = map_context red_fun gl.evar_env;
+    evar_hyps = map_named_context red_fun gl.evar_hyps;
     evar_body = gl.evar_body;
     evar_info = gl.evar_info }
 
@@ -181,7 +182,7 @@ let refiner = function
   | (Context ctxt) as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
-         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
+         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
          ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -197,7 +198,7 @@ let refiner = function
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
          let ctxt = out_some gl.evar_info in 
-         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
+         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
 	 ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -244,13 +245,13 @@ let extract_open_proof sigma pf =
             (fun id ->
                try let n = list_index id vl in (n,id)
 	       with Not_found -> failwith "caught")
-            (ids_of_named_context (evar_hyps goal)) in
+            (ids_of_named_context goal.evar_hyps) in
 	let sorted_rels =
 	  Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
 	let abs_concl =
           List.fold_right
             (fun (_,id) concl ->
-	       let (c,ty) = lookup_id id (evar_hyps goal) in
+	       let (c,ty) = lookup_id id goal.evar_hyps in
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl
 	in
@@ -796,38 +797,36 @@ let pr_rule = function
 exception Different
 
 (* We remove from the var context of env what is already in osign *)
-let thin_sign osign env =
-  process_named_context
-    (fun env (id,c,ty as d) ->
+let thin_sign osign sign =
+  Sign.fold_named_context
+    (fun (id,c,ty as d) sign ->
        try 
-	 if lookup_id id osign = (c,ty) then env
+	 if lookup_id id osign = (c,ty) then sign
 	 else raise Different
-       with Not_found | Different -> push_named_decl d env)
-    env
+       with Not_found | Different -> add_named_decl d sign)
+    sign empty_named_context
 
 let rec print_proof sigma osign pf =
-  let {evar_env=env; evar_concl=cl; 
+  let {evar_hyps=hyps; evar_concl=cl; 
        evar_info=info; evar_body=body} = pf.goal in
-  let env' = thin_sign osign env in
+  let hyps' = thin_sign osign hyps in
   match pf.ref with
     | None -> 
-	hOV 0 [< pr_seq {evar_env=env'; evar_concl=cl;
+	hOV 0 [< pr_seq {evar_hyps=hyps'; evar_concl=cl;
 			 evar_info=info; evar_body=body} >]
     | Some(r,spfl) ->
-  	let sign = named_context env in
-    	hOV 0 [< hOV 0 (pr_seq {evar_env=env'; evar_concl=cl;
+    	hOV 0 [< hOV 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl;
 				evar_info=info; evar_body=body});
 		 'sPC ; 'sTR" BY ";
 		 hOV 0 [< pr_rule r >]; 'fNL ;
 		 'sTR"  ";
-		 hOV 0 (prlist_with_sep pr_fnl (print_proof sigma sign) spfl)
+		 hOV 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)
               >]
 	  
 let pr_change gl = [< 'sTR"Change " ; prterm gl.evar_concl ; 'sTR"." ; 'fNL>]
 		     
 let rec print_script nochange sigma osign pf =
-  let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = named_context env in
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None ->
         if nochange then 
@@ -841,8 +840,7 @@ let rec print_script nochange sigma osign pf =
              (print_script nochange sigma sign) spfl >]
 
 let rec print_treescript sigma osign pf =
-  let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = named_context env in
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None -> [< >]
     | Some(r,spfl) ->
@@ -857,8 +855,7 @@ let rec print_treescript sigma osign pf =
 	>]
 
 let rec print_info_script sigma osign pf =
-  let {evar_env=env; evar_concl=cl} = pf.goal in
-  let sign = named_context env in
+  let {evar_hyps=sign; evar_concl=cl} = pf.goal in
   match pf.ref with
     | None -> [< >]
     | Some(r,spfl) ->
@@ -887,7 +884,7 @@ let tclINFO (tac : tactic) gls =
   let (sgl,v) as res = tac gls in 
   begin try 
     let pf = v (List.map leaf (sig_it sgl)) in
-    let sign = named_context (sig_it gls).evar_env in
+    let sign = (sig_it gls).evar_hyps in
     mSGNL(hOV 0 [< 'sTR" == "; 
                    print_subscript 
                      ((compose ts_it sig_sig) gls) sign pf >])
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6e0fafd8a..272fe6eae 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -35,8 +35,8 @@ 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 pf_env gls = (sig_it gls).evar_env
-let pf_hyps gls = named_context (sig_it gls).evar_env
+let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
+let pf_hyps gls = (sig_it gls).evar_hyps
 
 let pf_concl gls = (sig_it gls).evar_concl
 (*
@@ -64,23 +64,23 @@ let pf_ctxt gls      = get_ctxt (sig_it gls)
 
 let pf_interp_constr gls c =
   let evc = project gls in 
-  Astterm.interp_constr evc (sig_it gls).evar_env c
+  Astterm.interp_constr evc (pf_env gls) c
 
 let pf_interp_openconstr gls c =
   let evc = project gls in 
-  Astterm.interp_openconstr evc (sig_it gls).evar_env c
+  Astterm.interp_openconstr evc (pf_env gls) c
 
 let pf_interp_type gls c =
   let evc = project gls in 
-  Astterm.interp_type evc (sig_it gls).evar_env c
+  Astterm.interp_type evc (pf_env gls) c
 
-let pf_global gls id = Declare.construct_reference (sig_it gls).evar_env CCI id
+let pf_global gls id = Declare.construct_reference (pf_env gls) CCI id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
 let pf_execute gls =
   let evc = project gls in 
-  Typing.unsafe_machine (sig_it gls).evar_env evc
+  Typing.unsafe_machine (pf_env gls) evc
 
 let pf_reduction_of_redexp gls re c = 
   reduction_of_redexp re (pf_env gls) (project gls) c 
@@ -276,8 +276,8 @@ let mutual_cofix lf lar pf =
                   terms    = lar; params   = []}) pf
     
 let rename_bound_var_goal gls =
-  let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
-  let ids = ids_of_named_context (Environ.named_context env) in
+  let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in 
+  let ids = ids_of_named_context sign in
   convert_concl (rename_bound_var ids cl) gls
     
 
@@ -509,8 +509,8 @@ open Printer
 
 let pr_com sigma goal com =
   prterm (rename_bound_var 
-            (ids_of_named_context (named_context goal.evar_env)) 
-            (Astterm.interp_constr sigma goal.evar_env com))
+            (ids_of_named_context goal.evar_hyps) 
+            (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))
 
 let pr_one_binding sigma goal = function
   | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]