les variables existentielles contiennent maintenant un environnement (type

unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres
le module Environ.


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

13 files changed, 122 insertions, 94 deletions

diff --git a/.depend b/.depend
index 335018706e..27f9cef6f2 100644
--- a/.depend
+++ b/.depend
@@ -3,10 +3,11 @@ kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 kernel/constant.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \
+kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
+kernel/evd.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi 
 kernel/generic.cmi: kernel/names.cmi lib/util.cmi 
 kernel/indtypes.cmi: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
     kernel/term.cmi kernel/univ.cmi 
@@ -54,9 +55,10 @@ proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi 
-proofs/proof_trees.cmi: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
-    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi 
-proofs/refiner.cmi: proofs/proof_trees.cmi 
+proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
+    lib/util.cmi 
+proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
@@ -92,10 +94,10 @@ kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx lib/system.cmx kernel/term.cmx kernel/univ.cmx \
     lib/util.cmx kernel/environ.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/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/generic.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
     kernel/generic.cmi 
 kernel/generic.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
@@ -244,18 +246,18 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx lib/util.cmx \
     proofs/logic.cmi 
-proofs/proof_trees.cmo: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
-    kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi \
-    proofs/proof_trees.cmi 
-proofs/proof_trees.cmx: parsing/coqast.cmx kernel/evd.cmx kernel/names.cmx \
-    kernel/sign.cmx lib/stamps.cmx kernel/term.cmx lib/util.cmx \
-    proofs/proof_trees.cmi 
-proofs/refiner.cmo: toplevel/errors.cmi kernel/evd.cmi proofs/logic.cmi \
-    lib/pp.cmi proofs/proof_trees.cmi lib/stamps.cmi lib/util.cmi \
-    proofs/refiner.cmi 
-proofs/refiner.cmx: toplevel/errors.cmx kernel/evd.cmx proofs/logic.cmx \
-    lib/pp.cmx proofs/proof_trees.cmx lib/stamps.cmx lib/util.cmx \
-    proofs/refiner.cmi 
+proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
+    lib/util.cmi proofs/proof_trees.cmi 
+proofs/proof_trees.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/names.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
+    lib/util.cmx proofs/proof_trees.cmi 
+proofs/refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
+    lib/stamps.cmi kernel/term.cmi lib/util.cmi proofs/refiner.cmi 
+proofs/refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \
+    lib/stamps.cmx kernel/term.cmx lib/util.cmx proofs/refiner.cmi 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
diff --git a/Makefile b/Makefile
index 8c6c457062..09b189ca0e 100644
--- a/Makefile
+++ b/Makefile
@@ -36,9 +36,9 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
     lib/bstack.cmo lib/edit.cmo lib/stamps.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
-       kernel/sign.cmo kernel/constant.cmo kernel/evd.cmo \
+       kernel/sign.cmo kernel/constant.cmo \
        kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \
-       kernel/environ.cmo kernel/instantiate.cmo \
+       kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \
        kernel/closure.cmo kernel/reduction.cmo \
        kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
        kernel/typing.cmo
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 004ef8e536..a983a67597 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -50,6 +50,10 @@ let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 let push_var idvar env =
   { env with env_context = add_glob idvar env.env_context }
 
+let change_hyps f env =
+  let ctx = env.env_context in
+  { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) }
+
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 61fb4b64a6..d3fd22c01e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -4,7 +4,6 @@
 (*i*)
 open Names
 open Term
-open Evd
 open Constant
 open Inductive
 open Abstraction
@@ -25,7 +24,11 @@ val universes : unsafe_env -> universes
 val context : unsafe_env -> context
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
+val change_hyps : 
+  (typed_type signature -> typed_type signature) -> unsafe_env -> unsafe_env
+
 val push_rel : name * typed_type -> unsafe_env -> unsafe_env
+
 val set_universes : universes -> unsafe_env -> unsafe_env
 val add_constraints : constraints -> unsafe_env -> unsafe_env
 val add_constant : 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 270ad1f2e4..b31f2f6b79 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -5,6 +5,7 @@ open Util
 open Names
 open Term
 open Sign
+open Environ
 
 (* The type of mappings for existential variables *)
 
@@ -20,7 +21,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_hyps : typed_type signature;
+  evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
 
@@ -41,7 +42,7 @@ let define evd ev body =
   let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_hyps = oldinfo.evar_hyps;
+      evar_env = oldinfo.evar_env;
       evar_body = Evar_defined body;
       evar_info = oldinfo.evar_info } 
   in
@@ -66,3 +67,4 @@ let is_defined sigma ev =
 
 let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
 
+let evar_hyps ev = get_globals (context ev.evar_env)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 80e767fa85..df80ee72b7 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -5,6 +5,7 @@
 open Names
 open Term
 open Sign
+open Environ
 (*i*)
 
 (* The type of mappings for existential variables.
@@ -23,7 +24,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_hyps : typed_type signature;
+  evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
 
@@ -48,3 +49,5 @@ val is_evar : 'a evar_map -> evar -> bool
 val is_defined : 'a evar_map -> evar -> bool
 
 val metamap : 'a evar_map -> (int * constr) list
+
+val evar_hyps : 'a evar_info -> typed_type signature
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index acc48bcb05..0cdc50c562 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -71,13 +71,13 @@ let name_of_existential n = id_of_string ("?" ^ string_of_int n)
 let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
+  let hyps = evar_hyps info in
   instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
 
 let existential_value sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
+  let hyps = evar_hyps info in
   match info.evar_body with
     | Evar_defined c ->
 	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 37fce80b7e..e6f07410bd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -26,39 +26,39 @@ let conv_leq_goal env sigma arg ty conclty =
   if not (is_conv_leq env sigma ty conclty) then 
     raise (RefinerError (BadType (arg,ty,conclty)))
 
-let type_of env hyps c =
+let type_of env c =
   failwith "TODO: typage avec VE"
 
 let execute_type env ty =
   failwith "TODO: typage type avec VE"
 
-let rec mk_refgoals env sigma goal goalacc conclty trm =
-  let hyps = goal.evar_hyps in
+let rec mk_refgoals sigma goal goalacc conclty trm =
+  let env = goal.evar_env in
   match trm with
     | DOP0(Meta mv) ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
 	let ctxt = goal.evar_info in 
-	(mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty
+	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
-	let _ = type_of env hyps ty in
+	let _ = type_of env ty in
 	conv_leq_goal env sigma trm ty conclty;
-	mk_refgoals env sigma goal goalacc ty t
+	mk_refgoals sigma goal goalacc ty t
 
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
 	let (acc'',conclty') = 
-	  mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl) in
+	  mk_arggoals sigma goal acc' hdty (array_list_of_tl cl) in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in 
@@ -66,49 +66,51 @@ let rec mk_refgoals env sigma goal goalacc conclty trm =
 
     | t -> 
 	if occur_meta t then raise (RefinerError (OccurMeta t));
-      	let t'ty = type_of env hyps t in
+      	let t'ty = type_of env t in
 	conv_leq_goal env sigma t t'ty conclty;
         (goalacc,t'ty)
 
 (* Same as mkREFGOALS but without knowing te type of the term. Therefore,
  * Metas should be casted. *)
 
-and mk_hdgoals env sigma goal goalacc trm =
-  let hyps = goal.evar_hyps in
+and mk_hdgoals sigma goal goalacc trm =
+  let env = goal.evar_env in
   match trm with
     | DOP2(Cast,DOP0(Meta mv),ty) ->
-	let _ = type_of env hyps ty in
+	let _ = type_of env ty in
 	let ctxt = goal.evar_info in  
-	(mk_goal ctxt hyps (nf_betaiota env sigma ty))::goalacc,ty
+	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
 	  
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mk_hdgoals env sigma goal goalacc (array_hd cl) in
-	mk_arggoals env sigma goal acc' hdty (array_list_of_tl cl)
+	let (acc',hdty) = mk_hdgoals sigma goal goalacc (array_hd cl) in
+	mk_arggoals sigma goal acc' hdty (array_list_of_tl cl)
 	
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mk_casegoals env sigma goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
 	let acc'' = 
 	  array_fold_left2
-            (fun lacc ty fi -> fst (mk_refgoals env sigma goal lacc ty fi))
+            (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
             acc' lbrty lf 
 	in
 	(acc'',conclty')
 
-    | t -> goalacc,type_of env hyps t
+    | t -> goalacc,type_of env t
 
-and mk_arggoals env sigma goal goalacc funty = function
+and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
   | harg::tlargs ->
+      let env = goal.evar_env in
       (match whd_betadeltaiota env sigma funty with
 	 | DOP2(Prod,c1,b) ->
-	     let (acc',hargty) = mk_refgoals env sigma goal goalacc c1 harg in
-	     mk_arggoals env sigma goal acc' (sAPP b harg) tlargs
+	     let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
+	     mk_arggoals sigma goal acc' (sAPP b harg) tlargs
 	 | t -> raise (RefinerError (CannotApply (t,harg))))
 
-and mk_casegoals env sigma goal goalacc p c= 
-  let (acc',ct) = mk_hdgoals env sigma goal goalacc c in 
-  let (acc'',pt) = mk_hdgoals env sigma goal acc' p in
+and mk_casegoals sigma goal goalacc p c =
+  let env = goal.evar_env in
+  let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let (_,lbrty,conclty) = type_case_branches env sigma ct pt p c in
   (acc'',lbrty,conclty)
 
@@ -209,8 +211,9 @@ let move_after with_dep toleft (left,htfrom,right) hto =
     
 (* Primitive tactics are handled here *)
 
-let prim_refiner r env sigma goal =
-  let sign = goal.evar_hyps in
+let prim_refiner r sigma goal =
+  let env = goal.evar_env in
+  let sign = get_globals (context env) in
   let cl = goal.evar_concl in
   let info = goal.evar_info in
   match r with
@@ -221,7 +224,7 @@ let prim_refiner r env sigma goal =
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info (add_sign (id,a) sign) (sAPP b v) in 
+	       let sg = mk_goal info (push_var (id,a) env) (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -237,8 +240,8 @@ let prim_refiner r env sigma goal =
 		   "Can't introduce at that location: free variable conflict";
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info 
-			  (add_sign_after whereid (id,a) sign) (sAPP b v) in 
+	       let env' = change_hyps (add_sign_after whereid (id,a)) env in
+	       let sg = mk_goal info env' (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -256,8 +259,8 @@ let prim_refiner r env sigma goal =
 		   "Can't introduce at that location: free variable conflict";
 	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mk_goal info (add_sign_replacing id (id,a) sign) 
-			  (sAPP b v) in
+	       let env' = change_hyps (add_sign_replacing id (id,a)) env in
+	       let sg = mk_goal info env' (sAPP b v) in
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
@@ -278,7 +281,7 @@ let prim_refiner r env sigma goal =
      	let _ = check_ind n cl in 
 	if mem_sign sign f then error "name already used in the environment";
         let a = mk_assumption env sign cl in
-        let sg = mk_goal info (add_sign (f,a) sign) cl in
+        let sg = mk_goal info (push_var (f,a) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -307,7 +310,7 @@ let prim_refiner r env sigma goal =
 	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mk_goal info sign) (cl::lar)
+	      List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
@@ -330,21 +333,21 @@ let prim_refiner r env sigma goal =
 		error "name already used in the environment";
 	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf')
-	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
+	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
 	mk_sign sign (cl::lar,lf)
 	  
     | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
-	let (sgl,cl') = mk_refgoals env sigma goal [] cl c in
+	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	sgl
 
     | { name = Convert_concl; terms = [cl'] } ->
     	let cl'ty = type_of env sign cl' in
 	if is_conv_leq env sigma cl' cl then
-          let sg = mk_goal info sign (DOP2(Cast,cl',cl'ty)) in
+          let sg = mk_goal info env (DOP2(Cast,cl',cl'ty)) in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
@@ -353,7 +356,8 @@ let prim_refiner r env sigma goal =
       (* Faut-il garder la sorte d'origine ou celle du converti ?? *)
     	let tj = execute_type env (sign_before id sign) ty' in
 	if is_conv env sigma ty' (snd(lookup_sign id sign)).body then
-          [mk_goal info (modify_sign id tj sign) cl]
+	  let env' = change_hyps (modify_sign id tj) env in
+          [mk_goal info env' cl]
 	else 
 	  error "convert-hyp rule passed non-converting term"
 	    
@@ -376,7 +380,9 @@ let prim_refiner r env sigma goal =
             error ((string_of_id s) ^ " is used in the conclusion.");
           remove_pair s sign 
 	in
-     	let sg = mk_goal info (List.fold_left clear_aux sign ids) cl in
+	let env' = 
+	  change_hyps (fun sign -> List.fold_left clear_aux sign ids) env in
+     	let sg = mk_goal info env' cl in
      	[sg]
 
     | { name = Move withdep; hypspecs = ids } ->
@@ -386,7 +392,8 @@ let prim_refiner r env sigma goal =
   	let (left,right,typfrom,toleft) = split_sign hfrom hto hyps in
   	let hyps' = 
 	  move_after withdep toleft (left,(hfrom,typfrom),right) hto in
-  	[mk_goal info (make_sign hyps') cl]
+	let env' = change_hyps (fun _ -> make_sign hyps') env in
+  	[mk_goal info env' cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index cc9f108ee8..cbab2a90ca 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -9,7 +9,7 @@ open Environ
 open Proof_trees
 (*i*)
 
-val prim_refiner : prim_rule -> unsafe_env -> 'a evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
   ((typed_type, constr) env -> proof_tree -> constr) -> 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index eb9bc00f83..d12dad6e25 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -7,6 +7,7 @@ open Term
 open Sign
 open Evd
 open Stamps
+open Environ
 
 type bindOcc = 
   | Dep of identifier
@@ -93,9 +94,8 @@ let lc_toList lc = Intset.elements lc
 
 (* Functions on goals *)
 
-let mk_goal ctxt sign cl = 
-  { evar_hyps = sign; evar_concl = cl; evar_body = Evar_empty;
-    evar_info = ctxt }
+let mk_goal ctxt env cl = 
+  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
@@ -167,7 +167,7 @@ type global_constraints  = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  sign  : typed_type signature;
+  env   : unsafe_env;
   decls : evar_declarations }
 
 and readable_constraints = evar_recordty timestamped
@@ -175,21 +175,21 @@ and readable_constraints = evar_recordty timestamped
 (* Functions on readable constraints *)
 			     
 let mt_evcty lc gc = 
-  ts_mk { focus = lc; sign = nil_sign; decls = gc }
+  ts_mk { focus = lc; env = empty_env; decls = gc }
 
 let evc_of_evds evds gl = 
-  ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds }
+  ts_mk { focus = (get_lc gl); env = gl.evar_env; 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);
-                  sign  = evc.sign;
+                  env   = evc.env;
                   decls = Evd.add evc.decls k v })
     evc
 
-let get_hyps  evc = (ts_it evc).sign
+let get_env   evc = (ts_it evc).env
 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)
@@ -197,7 +197,7 @@ let get_gc    evc = (ts_mk (ts_it evc).decls)
 let remap evc (k,v) = 
   ts_mod
     (fun evc -> { focus = evc.focus;
-                  sign  = evc.sign;
+                  env   = evc.env;
                   decls = Evd.add evc.decls k v })
     evc
 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 69bc496046..b2d59fe63c 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -8,6 +8,7 @@ open Names
 open Term
 open Sign
 open Evd
+open Environ
 (*i*)
 
 (* This module declares the structure of proof trees, global and
@@ -98,13 +99,13 @@ and ctxtty = {
 type evar_declarations = ctxtty evar_map
 
 
-val mk_goal : ctxtty -> typed_type signature -> constr -> goal
+val mk_goal : ctxtty -> unsafe_env -> constr -> goal
 
 val mt_ctxt    : local_constraints -> ctxtty
-val get_ctxt   : goal  -> ctxtty
+val get_ctxt   : goal -> ctxtty
 val get_pgm    : goal -> constr option
 val set_pgm    : constr option -> ctxtty -> ctxtty
-val get_mimick : goal ->  proof_tree option
+val get_mimick : goal -> proof_tree option
 val set_mimick : proof_tree option ->  ctxtty -> ctxtty
 val get_lc     : goal -> local_constraints
 
@@ -129,14 +130,14 @@ type global_constraints = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  sign  : typed_type signature;
+  env  : unsafe_env;
   decls : evar_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 -> typed_type signature
+val get_env   : readable_constraints -> unsafe_env
 val get_focus : readable_constraints -> local_constraints
 val get_decls : readable_constraints -> evar_declarations
 val get_gc    : readable_constraints -> global_constraints
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 420af50ec9..4bd5836266 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -23,7 +23,7 @@ type validation_list = proof_tree list -> proof_tree list
 
 type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
 
-let hypotheses gl = gl.evar_hyps
+let hypotheses gl = gl.evar_env
 let conclusion gl = gl.evar_concl
 
 let sig_it x = x.it
@@ -132,9 +132,9 @@ let lookup_tactic s =
 let bad_subproof () =
   errorlabstrm "Refiner.refiner" [< 'sTR"Bad subproof in validation.">]
 
-let refiner env = function
+let refiner = function
   | Prim pr as r ->
-      let prim_fun = prim_refiner pr env in
+      let prim_fun = prim_refiner pr in
       (fun goal_sigma ->
          let sgl = prim_fun (ts_it goal_sigma.sigma) goal_sigma.it in 
 	 ({it=sgl; sigma = goal_sigma.sigma},
@@ -163,7 +163,7 @@ let refiner env = function
   | ((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
+         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
          ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -179,7 +179,7 @@ let refiner env = function
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
          let ctxt = gl.evar_info in 
-         let sg = mk_goal ctxt gl.evar_hyps gl.evar_concl in
+         let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
 	 ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
 	     let pf = List.hd pfl in
@@ -228,14 +228,14 @@ let extract_open_proof sign pf =
                match lookup_id id vl with
 		 | GLOBNAME _ -> failwith "caught"
 		 | RELNAME(n,_) -> (n,id))
-            (ids_of_sign goal.evar_hyps) in
+            (ids_of_sign (evar_hyps goal)) in
 	let sorted_rels = 
 	  Sort.list (fun (n1,_) (n2,_) -> n1>n2) visible_rels in
 	let abs_concl =
           List.fold_right
-            (fun (_,id) concl -> 
-	       mkNamedProd id (incast_type (snd(lookup_sign id goal.evar_hyps))) 
-		 concl)
+            (fun (_,id) concl ->
+	       let (_,ty) = lookup_sign id (evar_hyps goal) in
+	       mkNamedProd id (incast_type ty) concl)
             sorted_rels goal.evar_concl
 	in
 	let mv = new_meta() in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3e0b202c26..871c43a3ee 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 (*i*)
+open Term
+open Sign
 open Proof_trees
 (*i*)
 
@@ -34,3 +36,7 @@ val hide_tactic :
 
 val overwrite_hidden_tactic : 
   string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+val refiner : rule -> tactic
+
+val extract_open_proof : context -> proof_tree -> constr * (int * constr) list