- environment -> safe_environment

 - unsafe_env -> env


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

1 files changed, 22 insertions, 22 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ddf09ab348..4f47bfd886 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -20,26 +20,26 @@ val j_val_only : unsafe_judgment -> constr
    cosntructs the type type $c:t$, checking that $t$ is a sort. *)
 
 val typed_type_of_judgment : 
-  unsafe_env -> 'a evar_map -> unsafe_judgment -> typed_type
+  env -> 'a evar_map -> unsafe_judgment -> typed_type
 val assumption_of_judgment : 
-  unsafe_env -> 'a evar_map -> unsafe_judgment -> typed_type
+  env -> 'a evar_map -> unsafe_judgment -> typed_type
 
-val relative : unsafe_env -> int -> unsafe_judgment
+val relative : env -> int -> unsafe_judgment
 
-val type_of_constant : unsafe_env -> 'a evar_map -> constr -> typed_type
+val type_of_constant : env -> 'a evar_map -> constr -> typed_type
 
-val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type
+val type_of_inductive : env -> 'a evar_map -> constr -> typed_type
 
-val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr
+val type_of_constructor : env -> 'a evar_map -> constr -> constr
 
-val type_of_existential : unsafe_env -> 'a evar_map -> constr -> constr
+val type_of_existential : env -> 'a evar_map -> constr -> constr
 
-val type_of_case : unsafe_env -> 'a evar_map 
+val type_of_case : env -> 'a evar_map 
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment
 
 val type_case_branches :
-  unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
+  env -> 'a evar_map -> constr -> constr -> constr -> constr 
     -> constr * constr array * constr 
 
 val make_judge_of_prop_contents : contents -> unsafe_judgment
@@ -47,42 +47,42 @@ val make_judge_of_prop_contents : contents -> unsafe_judgment
 val make_judge_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
-  unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
+  env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val gen_rel :
-  unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
+  env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val cast_rel : 
-  unsafe_env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment 
+  env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment
 
 val apply_rel_list : 
-  unsafe_env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
+  env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
     -> unsafe_judgment * constraints
 
-val check_fix : unsafe_env -> 'a evar_map -> constr -> unit
-val check_cofix : unsafe_env -> 'a evar_map -> constr -> unit
+val check_fix : env -> 'a evar_map -> constr -> unit
+val check_cofix : env -> 'a evar_map -> constr -> unit
 
-val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array 
+val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
 
-val type_one_branch_dep : unsafe_env -> 'a evar_map -> 
+val type_one_branch_dep : env -> 'a evar_map -> 
   int * constr list * constr -> constr -> constr -> constr 
 
-val type_one_branch_nodep : unsafe_env -> 'a evar_map -> 
+val type_one_branch_nodep : env -> 'a evar_map -> 
   int * constr list * constr -> constr -> constr 
 
 val make_arity_dep : 
-  unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr 
+  env -> 'a evar_map -> constr -> constr -> constr -> constr 
 
 val make_arity_nodep : 
-  unsafe_env -> 'a evar_map -> constr -> constr -> constr 
+  env -> 'a evar_map -> constr -> constr -> constr 
 
 val find_case_dep_nparams :
-  unsafe_env -> 'a evar_map -> constr * constr ->
+  env -> 'a evar_map -> constr * constr ->
     constr * constr list ->
       constr -> bool * (int * constr list * constr list) 
 
-val type_inst_construct : unsafe_env -> 'a evar_map -> int -> constr -> constr 
+val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr