- environment -> safe_environment

 - unsafe_env -> env


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

6 files changed, 10 insertions, 10 deletions

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 0f121a9f2e..47bba83fa3 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -37,7 +37,7 @@ val w_Declare_At : evar -> evar -> constr -> w_tactic
 val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> evar_declarations
-val w_env        : walking_constraints -> unsafe_env
+val w_env        : walking_constraints -> env
 val w_type_of    : walking_constraints -> constr -> constr
 val w_add_sign   : (identifier * typed_type) -> walking_constraints 
                      -> walking_constraints
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f89c6e9b4e..a3e387b6e6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -401,7 +401,7 @@ let prim_refiner r sigma goal =
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
 let abst_value c =
-  let env = Global.unsafe_env () in
+  let env = Global.env () in
   Environ.abst_value env c
 	  
 let extract_constr = 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index ee0f3de895..067162e60e 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -168,7 +168,7 @@ type global_constraints  = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  env   : unsafe_env;
+  env   : env;
   decls : evar_declarations }
 
 and readable_constraints = evar_recordty timestamped
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 3801f9e4b4..7b612ac5fc 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -99,7 +99,7 @@ and ctxtty = {
 type evar_declarations = ctxtty evar_map
 
 
-val mk_goal : ctxtty -> unsafe_env -> constr -> goal
+val mk_goal : ctxtty -> env -> constr -> goal
 
 val mt_ctxt    : local_constraints -> ctxtty
 val get_ctxt   : goal -> ctxtty
@@ -130,14 +130,14 @@ type global_constraints = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  env   : unsafe_env;
+  env   : 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_env   : readable_constraints -> unsafe_env
+val get_env   : readable_constraints -> 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/tacmach.mli b/proofs/tacmach.mli
index ea13c75a79..be9761efdf 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -29,7 +29,7 @@ val apply_sig_tac :
   global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
 
 val pf_concl              : goal sigma -> constr
-val pf_env                : goal sigma -> unsafe_env
+val pf_env                : goal sigma -> env
 val pf_hyps               : goal sigma -> typed_type signature
 val pf_untyped_hyps       : goal sigma -> constr signature
 val pf_nth_hyp            : goal sigma -> int -> identifier * constr
@@ -178,7 +178,7 @@ val w_Declare           : section_path -> constr -> w_tactic
 val w_Declare_At        : section_path -> section_path -> constr -> w_tactic
 val w_Define            : section_path -> constr -> w_tactic
 val w_Underlying        : walking_constraints -> evar_declarations
-val w_env               : walking_constraints -> unsafe_env
+val w_env               : walking_constraints -> env
 val w_hyps              : walking_constraints -> context
 val w_type_of           : walking_constraints -> constr -> constr
 val w_add_sign          : (identifier * typed_type) 
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
index ccaaae4fb3..a1aec82cdd 100644
--- a/proofs/tacred.mli
+++ b/proofs/tacred.mli
@@ -18,10 +18,10 @@ val nf : 'a reduction_function
 val one_step_reduce : 'a reduction_function
 
 val reduce_to_mind : 
-  unsafe_env -> 'a evar_map -> constr -> constr * constr * constr
+  env -> 'a evar_map -> constr -> constr * constr * constr
 
 val reduce_to_ind : 
-  unsafe_env -> 'a evar_map -> constr -> section_path * constr * constr
+  env -> 'a evar_map -> constr -> section_path * constr * constr
 
 type red_expr =
   | Red