- environment -> safe_environment

 - unsafe_env -> env


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

14 files changed, 149 insertions, 149 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6dd6c2177..00aa0363f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -135,7 +135,7 @@ let red_under (md,r) rk =
 type ('a, 'b) infos = {
   i_flags : flags;
   i_repr : ('a, 'b) infos -> constr -> 'a;
-  i_env : unsafe_env;
+  i_env : env;
   i_evc : 'b evar_map;
   i_tab : (constr, 'a) Hashtbl.t }
 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index b928851ec..0cba4cb87 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -83,7 +83,7 @@ val fixp_reducible :
 
 (* normalization of a constr: the two functions to know... *)
 type 'a cbv_infos
-val create_cbv_infos : flags -> unsafe_env -> 'a evar_map -> 'a cbv_infos
+val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
 val cbv_norm : 'a cbv_infos -> constr -> constr
 
 (* recursive functions... *)
@@ -159,8 +159,8 @@ type case_status =
 
 (* Constant cache *)
 type 'a clos_infos
-val create_clos_infos : flags -> unsafe_env -> 'a evar_map -> 'a clos_infos
-val clos_infos_env : 'a clos_infos -> unsafe_env
+val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
+val clos_infos_env : 'a clos_infos -> env
 
 (* Reduction function *)
 val norm_val : 'a clos_infos -> fconstr -> constr
diff --git a/kernel/environ.ml b/kernel/environ.ml
index bed45797d..a6e878e6b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -26,7 +26,7 @@ type globals = {
   env_locals : (global * section_path) list;
   env_imports : import list }
 
-type unsafe_env = {
+type env = {
   env_context : context;
   env_globals : globals;
   env_universes : universes }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9f1c228a0..3c4dd633e 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -16,55 +16,55 @@ open Sign
    informations added in environments, and that is what we speak here
    of ``unsafe'' environments. *)
 
-type unsafe_env
+type env
 
-val empty_env : unsafe_env
+val empty_env : env
 
-val universes : unsafe_env -> universes
-val context : unsafe_env -> context
-val var_context : unsafe_env -> var_context
+val universes : env -> universes
+val context : env -> context
+val var_context : env -> var_context
 
-val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
+val push_var : identifier * typed_type -> env -> env
 val change_hyps : 
-  (typed_type signature -> typed_type signature) -> unsafe_env -> unsafe_env
+  (typed_type signature -> typed_type signature) -> env -> env
 
-val push_rel : name * typed_type -> unsafe_env -> unsafe_env
+val push_rel : name * typed_type -> env -> env
 
-val set_universes : universes -> unsafe_env -> unsafe_env
-val add_constraints : constraints -> unsafe_env -> unsafe_env
+val set_universes : universes -> env -> env
+val add_constraints : constraints -> env -> env
 val add_constant : 
-  section_path -> constant_body -> unsafe_env -> unsafe_env
+  section_path -> constant_body -> env -> env
 val add_mind : 
-  section_path -> mutual_inductive_body -> unsafe_env -> unsafe_env
+  section_path -> mutual_inductive_body -> env -> env
 val add_abstraction : 
-  section_path -> abstraction_body -> unsafe_env -> unsafe_env
+  section_path -> abstraction_body -> env -> env
 
 val new_meta : unit -> int
 
-val lookup_var : identifier -> unsafe_env -> name * typed_type
-val lookup_rel : int -> unsafe_env -> name * typed_type
-val lookup_constant : section_path -> unsafe_env -> constant_body
-val lookup_mind : section_path -> unsafe_env -> mutual_inductive_body
-val lookup_mind_specif : constr -> unsafe_env -> mind_specif
+val lookup_var : identifier -> env -> name * typed_type
+val lookup_rel : int -> env -> name * typed_type
+val lookup_constant : section_path -> env -> constant_body
+val lookup_mind : section_path -> env -> mutual_inductive_body
+val lookup_mind_specif : constr -> env -> mind_specif
 
-val id_of_global : unsafe_env -> sorts oper -> identifier
-val id_of_name_using_hdchar : unsafe_env -> constr -> name -> identifier
-val named_hd : unsafe_env -> constr -> name -> name
-val prod_name : unsafe_env -> name * constr * constr -> constr
+val id_of_global : env -> sorts oper -> identifier
+val id_of_name_using_hdchar : env -> constr -> name -> identifier
+val named_hd : env -> constr -> name -> name
+val prod_name : env -> name * constr * constr -> constr
 
-val translucent_abst : unsafe_env -> constr -> bool
-val evaluable_abst : unsafe_env -> constr -> bool
-val abst_value : unsafe_env -> constr -> constr
+val translucent_abst : env -> constr -> bool
+val evaluable_abst : env -> constr -> bool
+val abst_value : env -> constr -> constr
 
-val defined_constant : unsafe_env -> constr -> bool
-val evaluable_constant : unsafe_env -> constr -> bool
+val defined_constant : env -> constr -> bool
+val evaluable_constant : env -> constr -> bool
 
 (*s Modules. *)
 
 type compiled_env
 
-val export : unsafe_env -> string -> compiled_env
-val import : compiled_env -> unsafe_env -> unsafe_env
+val export : env -> string -> compiled_env
+val import : compiled_env -> env -> env
 
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 4599fbdc4..cc95958bc 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -21,7 +21,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : unsafe_env;
+  evar_env : env;
   evar_body : evar_body;
   evar_info : 'a }
 
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 6aba6f08d..1b00cddb4 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -24,7 +24,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : unsafe_env;
+  evar_env : env;
   evar_body : evar_body;
   evar_info : 'a }
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a77cc0921..421bc937c 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -12,12 +12,12 @@ open Environ
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
 
-val mind_check_arities : unsafe_env -> mutual_inductive_entry -> unit
+val mind_check_arities : env -> mutual_inductive_entry -> unit
 
-val sort_of_arity : unsafe_env -> constr -> sorts
+val sort_of_arity : env -> constr -> sorts
 
 val cci_inductive : 
-  unsafe_env -> unsafe_env -> path_kind -> int -> bool -> 
+  env -> env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 376494884..10d62cb85 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -16,13 +16,13 @@ val instantiate_constr :
 val instantiate_type : 
   identifier list -> typed_type -> constr list -> typed_type
 
-val constant_value : unsafe_env -> constr -> constr
-val constant_type : unsafe_env -> constr -> typed_type
+val constant_value : env -> constr -> constr
+val constant_type : env -> constr -> typed_type
 
 val existential_value : 'a evar_map -> constr -> constr
 val existential_type : 'a evar_map -> constr -> constr
 
-val const_abst_opt_value : unsafe_env -> 'a evar_map -> constr -> constr option
+val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option
 
 val mis_arity : mind_specif -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2ce121ed1..cbc3fe343 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -18,10 +18,10 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> 'a evar_map -> constr -> constr
+type 'a reduction_function = env -> 'a evar_map -> constr -> constr
 
 type 'a stack_reduction_function = 
-    unsafe_env -> 'a evar_map -> constr -> constr list -> constr * constr list
+    env -> 'a evar_map -> constr -> constr list -> constr * constr list
 
 (*************************************)
 (*** Reduction Functions Operators ***)
@@ -719,7 +719,7 @@ let pb_equal = function
   | CONV -> CONV
 
 type 'a conversion_function = 
-    unsafe_env -> 'a evar_map -> constr -> constr -> constraints
+    env -> 'a evar_map -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index a5244b680..572d4bcff 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -17,10 +17,10 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> 'a evar_map -> constr -> constr
+type 'a reduction_function = env -> 'a evar_map -> constr -> constr
 
 type 'a stack_reduction_function = 
-    unsafe_env -> 'a evar_map -> constr -> constr list -> constr * constr list
+    env -> 'a evar_map -> constr -> constr list -> constr * constr list
 
 val whd_stack : 'a stack_reduction_function
 
@@ -79,22 +79,22 @@ val whd_betadeltaiotaeta : 'a reduction_function
 val beta_applist : (constr * constr list) -> constr
 
 val hnf_prod_app : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
+  env -> 'a evar_map -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr array -> constr
+  env -> 'a evar_map -> string -> constr -> constr array -> constr
 val hnf_prod_applist : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr list -> constr
+  env -> 'a evar_map -> string -> constr -> constr list -> constr
 val hnf_lam_app : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
+  env -> 'a evar_map -> string -> constr -> constr -> constr
 val hnf_lam_appvect : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr array -> constr
+  env -> 'a evar_map -> string -> constr -> constr array -> constr
 val hnf_lam_applist : 
-  unsafe_env -> 'a evar_map -> string -> constr -> constr list -> constr
+  env -> 'a evar_map -> string -> constr -> constr list -> constr
 val splay_prod : 
-  unsafe_env -> 'a evar_map -> constr -> (name * constr) list * constr
-val decomp_prod : unsafe_env -> 'a evar_map -> constr -> int * constr
+  env -> 'a evar_map -> constr -> (name * constr) list * constr
+val decomp_prod : env -> 'a evar_map -> constr -> int * constr
 val decomp_n_prod : 
-  unsafe_env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
+  env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
@@ -104,17 +104,17 @@ type 'a miota_args = {
   mlf     : 'a array }  (* the branch code vector *)
 
 val reducible_mind_case : constr -> bool
-val reduce_mind_case : unsafe_env -> constr miota_args -> constr
-
-val is_arity : unsafe_env -> 'a evar_map -> constr -> bool
-val is_info_arity : unsafe_env -> 'a evar_map -> constr -> bool
-val is_info_sort : unsafe_env -> 'a evar_map -> constr -> bool
-val is_logic_arity : unsafe_env -> 'a evar_map -> constr -> bool
-val is_type_arity : unsafe_env -> 'a evar_map -> constr -> bool
-val is_info_type : unsafe_env -> 'a evar_map -> typed_type -> bool
-val is_info_cast_type : unsafe_env -> 'a evar_map -> constr -> bool
-val contents_of_cast_type : unsafe_env -> 'a evar_map -> constr -> contents
-val poly_args : unsafe_env -> 'a evar_map -> constr -> int list
+val reduce_mind_case : env -> constr miota_args -> constr
+
+val is_arity : env -> 'a evar_map -> constr -> bool
+val is_info_arity : env -> 'a evar_map -> constr -> bool
+val is_info_sort : env -> 'a evar_map -> constr -> bool
+val is_logic_arity : env -> 'a evar_map -> constr -> bool
+val is_type_arity : env -> 'a evar_map -> constr -> bool
+val is_info_type : env -> 'a evar_map -> typed_type -> bool
+val is_info_cast_type : env -> 'a evar_map -> constr -> bool
+val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
+val poly_args : env -> 'a evar_map -> constr -> int list
 
 val whd_programs : 'a reduction_function
 
@@ -152,7 +152,7 @@ val convert_forall2 :
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
 type 'a conversion_function = 
-    unsafe_env -> 'a evar_map -> constr -> constr -> constraints
+    env -> 'a evar_map -> constr -> constr -> constraints
 
 val fconv : conv_pb -> 'a conversion_function
 
@@ -163,16 +163,16 @@ val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> unsafe_env -> 'a evar_map -> constr array 
+  'a conversion_function -> env -> 'a evar_map -> constr array 
     -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> unsafe_env -> 'a evar_map
+  (int -> 'a conversion_function) -> env -> 'a evar_map
     -> constr array -> constr array -> constraints
 
-val is_conv : unsafe_env -> 'a evar_map -> constr -> constr -> bool
-val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
-val is_fconv : conv_pb -> unsafe_env -> 'a evar_map -> constr -> constr -> bool
+val is_conv : env -> 'a evar_map -> constr -> constr -> bool
+val is_conv_leq : env -> 'a evar_map -> constr -> constr -> bool
+val is_fconv : conv_pb -> env -> 'a evar_map -> constr -> constr -> bool
 
 
 (*s Special-Purpose Reduction Functions *)
@@ -194,18 +194,18 @@ val whd_ise1_metas : 'a evar_map -> constr -> constr
 
 (*s Obsolete Reduction Functions *)
 
-val hnf : unsafe_env -> 'a evar_map -> constr -> constr * constr list
+val hnf : env -> 'a evar_map -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
 val red_product : 'a reduction_function
 val find_mrectype : 
-  unsafe_env -> 'a evar_map -> constr -> constr * constr list
+  env -> 'a evar_map -> constr -> constr * constr list
 val find_minductype : 
-  unsafe_env -> 'a evar_map -> constr -> constr * constr list
+  env -> 'a evar_map -> constr -> constr * constr list
 val find_mcoinductype : 
-  unsafe_env -> 'a evar_map -> constr -> constr * constr list
-val check_mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
-val minductype_spec : unsafe_env -> 'a evar_map -> constr -> constr
-val mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
+  env -> 'a evar_map -> constr -> constr * constr list
+val check_mrectype_spec : env -> 'a evar_map -> constr -> constr
+val minductype_spec : env -> 'a evar_map -> constr -> constr
+val mrectype_spec : env -> 'a evar_map -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e523be510..04d63da8f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -227,7 +227,7 @@ let safe_machine_v env cv =
 
 (*s Safe environments. *)
 
-type environment = unsafe_env
+type safe_environment = env
 
 let empty_environment = empty_env
 
@@ -409,7 +409,7 @@ let add_constraints = add_constraints
 let export = export
 let import = import
 
-let unsafe_env_of_env e = e
+let env_of_safe_env e = e
 
 (*s Machines with information. *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 392040814..eae3f77df 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -15,37 +15,37 @@ open Typeops
 
 (*s Safe environments. Since we are now able to type terms, we can define an
   abstract type of safe environments, where objects are typed before being
-  added. Internally, the datatype is still [unsafe_env]. We re-export the
+  added. Internally, the datatype is still [env]. We re-export the
   functions of [Environ] for the new type [environment]. *)
 
-type environment
+type safe_environment
 
-val empty_environment : environment
+val empty_environment : safe_environment
 
-val universes : environment -> universes
-val context : environment -> context
-val var_context : environment -> var_context
+val universes : safe_environment -> universes
+val context : safe_environment -> context
+val var_context : safe_environment -> var_context
 
-val push_var : identifier * constr -> environment -> environment
-val push_rel : name * constr -> environment -> environment
+val push_var : identifier * constr -> safe_environment -> safe_environment
+val push_rel : name * constr -> safe_environment -> safe_environment
 val add_constant : 
-  section_path -> constant_entry -> environment -> environment
+  section_path -> constant_entry -> safe_environment -> safe_environment
 val add_parameter :
-  section_path -> constr -> environment -> environment
+  section_path -> constr -> safe_environment -> safe_environment
 val add_mind : 
-  section_path -> mutual_inductive_entry -> environment -> environment
-val add_constraints : constraints -> environment -> environment
+  section_path -> mutual_inductive_entry -> safe_environment -> safe_environment
+val add_constraints : constraints -> safe_environment -> safe_environment
 
-val lookup_var : identifier -> environment -> name * typed_type
-val lookup_rel : int -> environment -> name * typed_type
-val lookup_constant : section_path -> environment -> constant_body
-val lookup_mind : section_path -> environment -> mutual_inductive_body
-val lookup_mind_specif : constr -> environment -> mind_specif
+val lookup_var : identifier -> safe_environment -> name * typed_type
+val lookup_rel : int -> safe_environment -> name * typed_type
+val lookup_constant : section_path -> safe_environment -> constant_body
+val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
+val lookup_mind_specif : constr -> safe_environment -> mind_specif
 
-val export : environment -> string -> compiled_env
-val import : compiled_env -> environment -> environment
+val export : safe_environment -> string -> compiled_env
+val import : compiled_env -> safe_environment -> safe_environment
 
-val unsafe_env_of_env : environment -> unsafe_env
+val env_of_safe_env : safe_environment -> env
 
 (*s Typing without information. *)
 
@@ -55,20 +55,20 @@ val j_val : judgment -> constr
 val j_type : judgment -> constr
 val j_kind : judgment -> constr
 
-val safe_machine : environment -> constr -> judgment * constraints
-val safe_machine_type : environment -> constr -> typed_type
+val safe_machine : safe_environment -> constr -> judgment * constraints
+val safe_machine_type : safe_environment -> constr -> typed_type
 
-val fix_machine : environment -> constr -> judgment * constraints
-val fix_machine_type : environment -> constr -> typed_type
+val fix_machine : safe_environment -> constr -> judgment * constraints
+val fix_machine_type : safe_environment -> constr -> typed_type
 
-val unsafe_machine : environment -> constr -> judgment * constraints
-val unsafe_machine_type : environment -> constr -> typed_type
+val unsafe_machine : safe_environment -> constr -> judgment * constraints
+val unsafe_machine_type : safe_environment -> constr -> typed_type
 
-val type_of : environment -> constr -> constr
+val type_of : safe_environment -> constr -> constr
 
-val type_of_type : environment -> constr -> constr
+val type_of_type : safe_environment -> constr -> constr
 
-val unsafe_type_of : environment -> constr -> constr
+val unsafe_type_of : safe_environment -> constr -> constr
 
 
 (*s Typing with information (extraction). *)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index a3820217b..70f444987 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -36,49 +36,49 @@ type type_error =
 
 exception TypeError of path_kind * context * type_error
 
-val error_unbound_rel : path_kind -> unsafe_env -> int -> 'b
+val error_unbound_rel : path_kind -> env -> int -> 'b
 
-val error_cant_execute : path_kind -> unsafe_env -> constr -> 'b
+val error_cant_execute : path_kind -> env -> constr -> 'b
 
-val error_not_type : path_kind -> unsafe_env -> constr -> 'b
+val error_not_type : path_kind -> env -> constr -> 'b
 
-val error_assumption : path_kind -> unsafe_env -> constr -> 'b
+val error_assumption : path_kind -> env -> constr -> 'b
  
-val error_reference_variables : path_kind -> unsafe_env -> identifier -> 'b
+val error_reference_variables : path_kind -> env -> identifier -> 'b
 
 val error_elim_arity : 
-  path_kind -> unsafe_env -> constr -> constr list -> constr 
+  path_kind -> env -> constr -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> 'b
 
 val error_case_not_inductive : 
-  path_kind -> unsafe_env -> constr -> constr -> 'b
+  path_kind -> env -> constr -> constr -> 'b
 
 val error_number_branches : 
-  path_kind -> unsafe_env -> constr -> constr -> int -> 'b
+  path_kind -> env -> constr -> constr -> int -> 'b
 
 val error_ill_formed_branch :
-  path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
+  path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
 val error_generalization :
-  path_kind -> unsafe_env -> name * typed_type -> constr -> 'b
+  path_kind -> env -> name * typed_type -> constr -> 'b
 
 val error_actual_type :
-  path_kind -> unsafe_env -> constr -> constr -> constr -> 'b
+  path_kind -> env -> constr -> constr -> constr -> 'b
 
 val error_cant_apply : 
-  path_kind -> unsafe_env -> string -> unsafe_judgment 
+  path_kind -> env -> string -> unsafe_judgment 
     -> unsafe_judgment list -> 'b
 
 val error_ill_formed_rec_body :
-  path_kind -> unsafe_env -> std_ppcmds
+  path_kind -> env -> std_ppcmds
     -> name list -> int -> constr array -> 'b
 
 val error_ill_typed_rec_body  :
-  path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array 
+  path_kind -> env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> 'b
 
-val error_not_inductive : path_kind -> unsafe_env -> constr -> 'a
+val error_not_inductive : path_kind -> env -> constr -> 'a
 
-val error_ml_case : path_kind -> unsafe_env -> 
+val error_ml_case : path_kind -> env -> 
   string -> constr -> constr -> constr -> constr -> 'a
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ddf09ab34..4f47bfd88 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