- 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, 22 insertions, 22 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 0dcdf3dd28..9a32c1d461 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -252,7 +252,7 @@ let mind_path = function
 (* Eliminations. *)
 
 let declare_eliminations sp =
-  let env = Global.unsafe_env () in
+  let env = Global.env () in
   let sigma = Evd.empty in
   let mindid = basename sp in
   let mind = global_reference (kind_of_path sp) mindid in
diff --git a/library/global.ml b/library/global.ml
index 0fc1852cb9..5cefe53f6d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -14,9 +14,9 @@ open Summary
 
 let global_env = ref empty_environment
 
-let env () = !global_env
+let safe_env () = !global_env
 
-let unsafe_env () = unsafe_env_of_env !global_env
+let env () = env_of_safe_env !global_env
 
 let _ = 
   declare_summary "Global environment"
@@ -48,7 +48,7 @@ let import cenv = global_env := import cenv !global_env
 
 (* Some instanciations of functions from [Environ]. *)
 
-let id_of_global = Environ.id_of_global (unsafe_env_of_env !global_env)
+let id_of_global = Environ.id_of_global (env_of_safe_env !global_env)
 
 (* Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *)
 
diff --git a/library/global.mli b/library/global.mli
index 3e557b350b..a61b09c58f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -16,8 +16,8 @@ open Safe_typing
    The functions below are exactly the same as the ones in [Typing],
    operating on that global environment. *)
 
-val env : unit -> environment
-val unsafe_env : unit -> unsafe_env
+val safe_env : unit -> safe_environment
+val env : unit -> env
 
 val universes : unit -> universes
 val context : unit -> context
diff --git a/library/impargs.ml b/library/impargs.ml
index 8fe93b97c1..2cc34c3cb4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -17,7 +17,7 @@ let implicit_args = ref false
 
 let auto_implicits ty =
   if !implicit_args then
-    let genv = Global.unsafe_env() in
+    let genv = Global.env() in
     Impl_auto (poly_args genv Evd.empty ty)
   else
     No_impl
diff --git a/library/indrec.mli b/library/indrec.mli
index da2ae3102c..f1d1b51904 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -11,43 +11,43 @@ open Evd
 
 (* Eliminations. *)
 
-val make_case_dep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
-val make_case_nodep : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
-val make_case_gen : unsafe_env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_dep : env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_nodep : env -> 'a evar_map -> constr -> sorts -> constr
+val make_case_gen : env -> 'a evar_map -> constr -> sorts -> constr
 
-val make_indrec : unsafe_env -> 'a evar_map -> 
+val make_indrec : env -> 'a evar_map -> 
   (mind_specif * bool * sorts) list -> constr -> constr array
 
-val mis_make_indrec : unsafe_env -> 'a evar_map -> 
+val mis_make_indrec : env -> 'a evar_map -> 
   (mind_specif * bool * sorts) list -> mind_specif -> constr array
 
 val instanciate_indrec_scheme : sorts -> int -> constr -> constr
 
 val build_indrec : 
-  unsafe_env -> 'a evar_map -> (constr * bool * sorts) list -> constr array
+  env -> 'a evar_map -> (constr * bool * sorts) list -> constr array
 
-val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr 
+val type_rec_branches : bool -> env -> 'c evar_map -> constr 
   -> constr -> constr -> constr -> constr * constr array * constr
 
 val make_rec_branch_arg : 
-  unsafe_env -> 'a evar_map ->
+  env -> 'a evar_map ->
     constr array * ('b * constr) option array * int ->
     constr -> constr -> recarg list -> constr
 
 (*i Info pour JCF : déplacé dans pretyping, sert à Program
-val transform_rec : unsafe_env -> 'c evar_map -> (constr array) 
+val transform_rec : env -> 'c evar_map -> (constr array) 
   -> (constr * constr) -> constr
 i*)
 
-val is_mutind : unsafe_env -> 'a evar_map -> constr -> bool 
+val is_mutind : env -> 'a evar_map -> constr -> bool 
 
 val branch_scheme : 
-  unsafe_env -> 'a evar_map -> bool -> int -> constr -> constr
+  env -> 'a evar_map -> bool -> int -> constr -> constr
 
-val pred_case_ml : unsafe_env -> 'c evar_map -> bool -> (constr * constr) 
+val pred_case_ml : env -> 'c evar_map -> bool -> (constr * constr) 
   ->  constr array -> (int*constr)  ->constr
 
-val pred_case_ml_onebranch : unsafe_env ->'c evar_map -> bool ->
+val pred_case_ml_onebranch : env ->'c evar_map -> bool ->
   constr * constr ->int * constr * constr -> constr 
 
 val make_case_ml :
@@ -56,4 +56,4 @@ val make_case_ml :
 
 (*s Auxiliary functions. TODO: les déplacer ailleurs. *)
 
-val prod_create : unsafe_env -> constr * constr -> constr
+val prod_create : env -> constr * constr -> constr
diff --git a/library/redinfo.ml b/library/redinfo.ml
index dd1f32bd13..7cc35efca3 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -29,7 +29,7 @@ exception Elimconst
 
 let compute_consteval c = 
   let rec srec n labs c =
-    match whd_betadeltaeta_stack (Global.unsafe_env()) Evd.empty c [] with 
+    match whd_betadeltaeta_stack (Global.env()) Evd.empty c [] with 
       | (DOP2(Lambda, t, DLAM(_,g)), []) -> 
 	  srec (n+1) (t::labs) g
       | (DOPN(Fix (nv,i), bodies), l) ->