correction Abstract (et make world passe!)

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

21 files changed, 199 insertions, 170 deletions

diff --git a/.depend b/.depend
index 6f84cc27f..199dc09e5 100644
--- a/.depend
+++ b/.depend
@@ -4,8 +4,7 @@ kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
 kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi 
-kernel/evd.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi 
+kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
@@ -220,10 +219,10 @@ kernel/environ.cmo: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
 kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     kernel/environ.cmi 
-kernel/evd.cmo: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
-    kernel/term.cmi lib/util.cmi kernel/evd.cmi 
-kernel/evd.cmx: kernel/environ.cmx kernel/names.cmx kernel/sign.cmx \
-    kernel/term.cmx lib/util.cmx kernel/evd.cmi 
+kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
+    kernel/evd.cmi 
+kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
+    kernel/evd.cmi 
 kernel/indtypes.cmo: kernel/declarations.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/inductive.cmi kernel/instantiate.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
@@ -564,13 +563,13 @@ pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/evarutil.cmx kernel/evd.cmx kernel/instantiate.cmx \
     kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \
     kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi 
-pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi library/indrec.cmi \
-    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+    library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
     pretyping/evarutil.cmi 
-pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx library/indrec.cmx \
-    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+    library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
     pretyping/evarutil.cmi 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 64602f870..548f8b14a 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -5,7 +5,6 @@ open Util
 open Names
 open Term
 open Sign
-open Environ
 
 (* The type of mappings for existential variables *)
 
@@ -21,7 +20,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : env;
+  evar_hyps : named_context;
   evar_body : evar_body;
   evar_info : 'a option }
 
@@ -42,7 +41,7 @@ let define evd ev body =
   let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_env = oldinfo.evar_env;
+      evar_hyps = oldinfo.evar_hyps;
       evar_body = Evar_defined body;
       evar_info = oldinfo.evar_info } 
   in
@@ -65,7 +64,6 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let evar_hyps ev = named_context ev.evar_env
 let evar_body ev = ev.evar_body
 
 let id_of_existential ev =
diff --git a/kernel/evd.mli b/kernel/evd.mli
index e74474835..6ab60e295 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -5,13 +5,12 @@
 open Names
 open Term
 open Sign
-open Environ
 (*i*)
 
 (* The type of mappings for existential variables.
    The keys are integers and the associated information is a record
-   containing the type of the evar ([evar_concl]), the environment under which 
-   it was introduced ([evar_env]) and its definition ([evar_body]). 
+   containing the type of the evar ([evar_concl]), the context under which 
+   it was introduced ([evar_hyps]) and its definition ([evar_body]). 
    [evar_info] is used to add any other kind of information. *)
 
 type evar = int
@@ -24,7 +23,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : env;
+  evar_hyps : named_context;
   evar_body : evar_body;
   evar_info : 'a option }
 
@@ -48,7 +47,6 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val evar_hyps : 'a evar_info -> named_context
 val evar_body : 'a evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index e433423c0..f99ccb0c4 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -61,7 +61,7 @@ let name_of_existential n = id_of_string ("?" ^ string_of_int n)
 
 let existential_type sigma (n,args) =
   let info = Evd.map sigma n in
-  let hyps = evar_hyps info in
+  let hyps = info.evar_hyps in
   (* TODO: check args [this comment was in Typeops] *)
   instantiate_constr hyps info.evar_concl (Array.to_list args)
 
@@ -69,7 +69,7 @@ exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
-  let hyps = evar_hyps info in
+  let hyps = info.evar_hyps in
   match evar_body info with
     | Evar_defined c ->
 	instantiate_constr hyps c (Array.to_list args)
diff --git a/library/global.ml b/library/global.ml
index 118a189c6..7b69ca0a8 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -5,6 +5,7 @@ open Util
 open Term
 open Instantiate
 open Sign
+open Environ
 open Safe_typing
 open Summary
 
@@ -54,6 +55,12 @@ let import cenv = global_env := import cenv !global_env
 
 let id_of_global id = Environ.id_of_global (env_of_safe_env !global_env) id
 
+(*s Function to get an environment from the constants part of the global
+    environment and a given context. *)
+
+let env_of_context hyps = 
+  change_hyps (fun _ -> hyps) (env_of_safe_env !global_env)
+
 (* Functions of [Inductive], composed with [lookup_mind_specif]. *)
 (* Rem:Cannot open Inductive to avoid clash with Inductive.lookup_mind_specif*)
 
diff --git a/library/global.mli b/library/global.mli
index e9a9503ff..a59c99823 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,6 +46,11 @@ val import : compiled_env -> unit
 
 val id_of_global : global_reference -> identifier
 
+(*s Function to get an environment from the constants part of the global
+    environment and a given context. *)
+
+val env_of_context : named_context -> env
+
 (*s Re-exported functions of [Inductive], composed with 
     [lookup_mind_specif]. *)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 72e46b52b..080754172 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -38,6 +38,8 @@ let filter_sign p sign x =
     (x,[],nil_sign)
 *)
 
+let evar_env evd = Global.env_of_context evd.evar_hyps
+
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -48,7 +50,7 @@ let new_isevar_sign env sigma typ instance =
   if not (list_distinct (ids_of_named_context sign)) then 
     error "new_isevar_sign: two vars have the same name";
   let newev = Evd.new_evar() in
-  let info = { evar_concl = typ; evar_env = env; 
+  let info = { evar_concl = typ; evar_hyps = sign; 
 	       evar_body = Evar_empty; evar_info = None } in
   (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance))
 
@@ -71,9 +73,9 @@ let new_type_var env sigma =
 let split_evar_to_arrow sigma c =
   let (ev,args) = destEvar c in
   let evd = Evd.map sigma ev in
-  let evenv = evd.evar_env in
+  let evenv = evar_env evd in
   let (sigma1,dom) = new_type_var evenv sigma in
-  let hyps = named_context evenv in
+  let hyps = evd.evar_hyps in
   let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
   let newenv = push_named_assum (nvar, dom) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
@@ -98,8 +100,8 @@ let do_restrict_hyps sigma c =
   let (ev,args) = destEvar c in
   let args = Array.to_list args in
   let evd = Evd.map sigma ev in
-  let env = evd.evar_env in
-  let hyps = named_context env in
+  let env = evar_env evd in
+  let hyps = evd.evar_hyps in
   let (_,(rsign,ncargs)) =
     List.fold_left 
       (fun (sign,(rs,na)) a ->
@@ -248,7 +250,7 @@ let evar_define isevars (ev,argsv) rhs =
   let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
-  let worklist = make_subst evd.evar_env args in
+  let worklist = make_subst (evar_env evd) args in
   let body = real_clean isevars ev worklist rhs in
   ise_define isevars ev body;
   [ev]
@@ -349,8 +351,8 @@ let get_changed_pb lev =
 let solve_refl conv_algo env isevars ev argsv1 argsv2 =
   if argsv1 = argsv2 then [] else
   let evd = Evd.map !isevars ev in
-  let env = evd.evar_env in
-  let hyps = named_context env in
+  let env = evar_env evd in
+  let hyps = evd.evar_hyps in
   let (_,rsign) = 
     array_fold_left2
       (fun (sgn,rsgn) a1 a2 ->
@@ -361,10 +363,9 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
       (hyps,[]) argsv1 argsv2 
   in
   let nsign = List.rev rsign in
-  let nenv = change_hyps (fun _ -> nsign) env in
   let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in
   let newev = Evd.new_evar () in
-  let info = { evar_concl = evd.evar_concl; evar_env = nenv;
+  let info = { evar_concl = evd.evar_concl; evar_hyps = nsign;
 	       evar_body = Evar_empty; evar_info = None } in
   isevars :=
     Evd.define (Evd.add !isevars newev info) ev (mkEvar (newev,nargs));
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 069a0f176..6e70539ca 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -12,6 +12,8 @@ open Reduction
 
 (*s This modules provides useful functions for unification modulo evars *)
 
+val evar_env : 'a evar_info -> env
+
 val dummy_sort : constr
 type evar_constraint = conv_pb * constr * constr
 type 'a evar_defs = 'a evar_map ref
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 >]
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 962c18cc1..d562b0ed9 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -188,15 +188,21 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ind =
     try find_rectype env sigma i
     with Induc ->
-      errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in
+      errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) 
+  in
   let (invEnv,invGoal) =
-    compute_first_inversion_scheme env sigma ind sort dep_option in
-  assert (list_subset (global_vars invGoal) (ids_of_named_context (named_context invEnv)));
-(*
+    compute_first_inversion_scheme env sigma ind sort dep_option 
+  in
+  assert 
+    (list_subset 
+       (global_vars invGoal) 
+       (ids_of_named_context (named_context invEnv)));
+  (*
     errorlabstrm "lemma_inversion"
-      [< 'sTR"Computed inversion goal was not closed in initial signature" >];
-*)
-  let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invEnv invGoal) in
+    [< 'sTR"Computed inversion goal was not closed in initial signature" >];
+  *)
+  let invSign = named_context invEnv in
+  let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invSign invGoal) in
   let pfs =
     solve_pftreestate (tclTHEN intro 
 			 (onLastHyp (compose inv_op out_some))) pfs in
@@ -207,16 +213,19 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       (fun env (id,_,_ as d) sign ->
          if mem_named_context id global_named_context then sign
 	 else add_named_decl d sign)
-      invEnv empty_named_context in
+      invEnv empty_named_context 
+  in
   let (_,ownSign,mvb) =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
 	 (h::avoid, add_named_assum (h,mvty) sign, (mv,mkVar h)::mvb))
       (ids_of_context invEnv, ownSign, [])
-      meta_types in
+      meta_types 
+  in
   let invProof = 
-    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign in
+    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign 
+  in
   invProof
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5a5500fdc..018197dd4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -120,7 +120,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 (sig_it gls).Evd.evar_env (Stamps.ts_it (sig_sig gls)) pat n
+  matches_conv (pf_env gls) (Stamps.ts_it (sig_sig 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 34ad6e56c..8b9a8d0af 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1653,9 +1653,8 @@ let abstract_subproof name tac gls =
              (ids_of_named_context global_sign) in
   let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t)
                 (pf_concl gls) sign in
-  let env' = change_hyps (fun _ -> current_sign) env in
   let lemme =
-    start_proof na Declare.NeverDischarge env' concl;
+    start_proof na Declare.NeverDischarge current_sign concl;
     let _,(const,strength) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 577c29b05..d51cf629c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -366,13 +366,14 @@ let build_scheme lnamedepindsort =
 
 let start_proof_com sopt stre com =
   let env = Global.env () in
+  let sign = Global.named_context () in
   let id = match sopt with
     | Some id -> id
     | None ->
 	next_ident_away (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
   in
-  Pfedit.start_proof id stre env (interp_type Evd.empty env com)
+  Pfedit.start_proof id stre sign (interp_type Evd.empty env com)
 
 let save_named opacity =
   let id,(const,strength) = Pfedit.cook_proof () in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8d109ab7e..dffccf3f9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -557,7 +557,7 @@ let _ =
 	      let (pfterm,_) = extract_open_pftreestate pts in
 	      let message = 
 		try 
-		  Typeops.control_only_guard pf.goal.evar_env 
+		  Typeops.control_only_guard (Evarutil.evar_env pf.goal)
 		    Evd.empty pfterm; 
 		  [< 'sTR "The condition holds up to here" >]
                 with UserError(_,s) ->