- environment -> safe_environment

 - unsafe_env -> env


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

9 files changed, 42 insertions, 42 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 25163f6e6a..8c2f848878 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -45,7 +45,7 @@ val cte_of_constr : constr -> cte_typ
 val class_info : cl_typ -> (int * cl_info_typ)
 val coercion_info : coe_typ -> (int * coe_info_typ)
 val constructor_at_head : constr -> cl_typ * int
-val class_of : unsafe_env -> 'c evar_map -> constr -> constr * int
+val class_of : env -> 'c evar_map -> constr -> constr * int
 val class_args_of : constr -> constr list
 val inClass : (cl_typ * cl_info_typ) -> obj
 val outClass : obj -> (cl_typ * cl_info_typ)
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 3fc8dfb91d..c510299acf 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -12,17 +12,17 @@ open Evarutil
 (* Coercions. *)
 
 val inh_app_fun :
-  unsafe_env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_tosort_force :
-  unsafe_env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_tosort :
-  unsafe_env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_ass_of_j : unsafe_env -> 'a evar_defs ->
+  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+val inh_ass_of_j : env -> 'a evar_defs ->
   unsafe_judgment -> typed_type
-val inh_coerce_to : unsafe_env -> 'a evar_defs ->
+val inh_coerce_to : env -> 'a evar_defs ->
   constr -> unsafe_judgment -> unsafe_judgment
-val inh_cast_rel : unsafe_env -> 'a evar_defs ->
+val inh_cast_rel : env -> 'a evar_defs ->
   unsafe_judgment -> unsafe_judgment -> unsafe_judgment
-val inh_apply_rel_list : bool -> unsafe_env -> 'a evar_defs ->
+val inh_apply_rel_list : bool -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) 
     -> unsafe_judgment
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 59dfc7895c..9310e5dd38 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -11,18 +11,18 @@ open Evarutil
 
 val reset_problems : unit -> unit
 
-val the_conv_x : unsafe_env -> unit evar_defs -> constr -> constr -> bool
+val the_conv_x : env -> unit evar_defs -> constr -> constr -> bool
 
-val the_conv_x_leq : unsafe_env -> unit evar_defs -> constr -> constr -> bool
+val the_conv_x_leq : env -> unit evar_defs -> constr -> constr -> bool
 
 (* For debugging *)
 val solve_pb : 
-  unsafe_env -> unit evar_defs -> conv_pb * constr * constr -> bool
+  env -> unit evar_defs -> conv_pb * constr * constr -> bool
 
 val evar_conv_x : 
-  unsafe_env -> unit evar_defs ->
+  env -> unit evar_defs ->
     conv_pb -> constr -> constr -> bool
 
 val evar_eqappr_x : 
-  unsafe_env -> unit evar_defs ->
+  env -> unit evar_defs ->
     conv_pb -> constr * constr list -> constr * constr list -> bool
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3cbf887c57..501e9f28ec 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -35,7 +35,7 @@ val ise_defined : 'a evar_defs -> constr -> bool
 val real_clean :
   unit evar_defs -> int -> (identifier * constr) list -> constr -> constr
 val new_isevar :
-  unit evar_defs -> unsafe_env -> constr -> path_kind -> constr * constr
+  unit evar_defs -> env -> constr -> path_kind -> constr * constr
 val evar_define : unit evar_defs -> constr -> constr -> int list
 val solve_simple_eqn : (constr -> constr -> bool) -> unit evar_defs ->
   (conv_pb * constr * constr) -> int list option
@@ -59,15 +59,15 @@ val mk_tycon2 : trad_constraint -> constr -> trad_constraint
 
 (* application *)
 val app_dom_tycon : 
-  unsafe_env -> unit evar_defs -> trad_constraint -> trad_constraint
+  env -> unit evar_defs -> trad_constraint -> trad_constraint
 val app_rng_tycon :
-  unsafe_env -> 'a evar_defs -> constr -> trad_constraint -> trad_constraint
+  env -> 'a evar_defs -> constr -> trad_constraint -> trad_constraint
 
 (* abstraction *)
 val abs_dom_valcon : 
-  unsafe_env -> unit evar_defs -> trad_constraint -> trad_constraint
+  env -> unit evar_defs -> trad_constraint -> trad_constraint
 val abs_rng_tycon : 
-  unsafe_env -> 'a evar_defs -> trad_constraint -> trad_constraint
+  env -> 'a evar_defs -> trad_constraint -> trad_constraint
 
 
 (* $Id$ *)
diff --git a/pretyping/multcase.mli b/pretyping/multcase.mli
index 68e68c1b44..c0997c044e 100644
--- a/pretyping/multcase.mli
+++ b/pretyping/multcase.mli
@@ -13,8 +13,8 @@ open Evarutil
 (* Compilation of pattern-matching. *)
 
 val compile_multcase :
-  (trad_constraint -> unsafe_env -> rawconstr -> unsafe_judgment)
-  * 'a evar_defs -> trad_constraint -> unsafe_env ->
+  (trad_constraint -> env -> rawconstr -> unsafe_judgment)
+  * 'a evar_defs -> trad_constraint -> env ->
     rawconstr option * rawconstr list *
     (identifier list * pattern list * rawconstr) list ->
     unsafe_judgment
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 4e37b18a75..33238ecd9e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -16,16 +16,16 @@ open Rawterm
 exception PretypeError of loc * path_kind * context * type_error
 
 val error_cant_find_case_type_loc : 
-  loc -> unsafe_env -> constr -> 'a
+  loc -> env -> constr -> 'a
 
 val error_ill_formed_branch_loc : 
-  loc -> path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
+  loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc : 
-  loc -> path_kind -> unsafe_env -> constr -> constr -> int -> 'b
+  loc -> path_kind -> env -> constr -> constr -> int -> 'b
 
-val error_occur_check : path_kind -> unsafe_env -> int -> constr -> 'a
+val error_occur_check : path_kind -> env -> int -> constr -> 'a
 
-val error_not_clean : path_kind -> unsafe_env -> int -> constr -> 'a
+val error_not_clean : path_kind -> env -> int -> constr -> 'a
 
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 84097f8581..995779783a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -14,24 +14,24 @@ open Evarutil
 (* Typing with Trad, and re-checking with Mach *)
 (*i
 val infconstruct_type :
-  'c evar_map -> (unsafe_env * unsafe_env) ->
+  'c evar_map -> (env * env) ->
     Coqast.t -> typed_type * information
 val infconstruct :
-  'c evar_map -> (unsafe_env * unsafe_env) ->
+  'c evar_map -> (env * env) ->
     Coqast.t -> unsafe_judgment * information
 
 (* Typing, re-checking with universes constraints *)
 val fconstruct_with_univ :
-  'c evar_map -> unsafe_env -> Coqast.t -> unsafe_judgment
-val fconstruct_with_univ_sp : 'c evar_map -> unsafe_env
+  'c evar_map -> env -> Coqast.t -> unsafe_judgment
+val fconstruct_with_univ_sp : 'c evar_map -> env
   -> section_path -> constr -> Impuniv.universes * unsafe_judgment
-val fconstruct_type_with_univ_sp : 'c evar_map -> unsafe_env
+val fconstruct_type_with_univ_sp : 'c evar_map -> env
   -> section_path -> constr -> Impuniv.universes * typed_type
 val infconstruct_with_univ_sp :
-  'c evar_map -> (unsafe_env * unsafe_env)
+  'c evar_map -> (env * env)
   -> section_path -> constr -> Impuniv.universes * (unsafe_judgment * information)
 val infconstruct_type_with_univ_sp :
-  'c evar_map -> (unsafe_env * unsafe_env)
+  'c evar_map -> (env * env)
   -> section_path -> constr 
   -> Impuniv.universes * (typed_type * information)
 i*)
@@ -41,24 +41,24 @@ i*)
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
  * on unresolved evars, or replace them by Metas *)
 val ise_resolve : bool -> unit evar_map -> (int * constr) list ->
-  unsafe_env -> rawconstr -> unsafe_judgment
+  env -> rawconstr -> unsafe_judgment
 val ise_resolve_type : bool -> unit evar_map -> (int * constr) list ->
-  unsafe_env -> rawconstr -> typed_type
+  env -> rawconstr -> typed_type
 
 (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
  * if we must coerce to a type *)
-val ise_resolve1 : bool -> unit evar_map -> unsafe_env -> rawconstr -> constr
+val ise_resolve1 : bool -> unit evar_map -> env -> rawconstr -> constr
 
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
  *)
 val ise_resolve_nocheck : unit evar_map -> (int * constr) list ->
-  unsafe_env -> rawconstr -> unsafe_judgment
+  env -> rawconstr -> unsafe_judgment
 
 
 (* Internal of Trad...
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
-  trad_constraint -> unsafe_env -> unit evar_defs -> rawconstr 
+  trad_constraint -> env -> unit evar_defs -> rawconstr 
     -> unsafe_judgment
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index e49171a2ac..8304434d8a 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -4,6 +4,6 @@ open Term
 open Evd
 open Environ
 
-val get_type_of : unsafe_env -> 'a evar_map -> constr -> constr
-val get_sort_of : unsafe_env -> 'a evar_map -> constr -> sorts
+val get_type_of : env -> 'a evar_map -> constr -> constr
+val get_sort_of : env -> 'a evar_map -> constr -> sorts
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index b12cd369d3..80fcc5ec99 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -10,9 +10,9 @@ open Evd
 (* This module provides the typing machine with existential variables
    (but without universes). *)
 
-val type_of : unsafe_env -> 'a evar_map -> constr -> constr
+val type_of : env -> 'a evar_map -> constr -> constr
 
-val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type
+val execute_type : env -> 'a evar_map -> constr -> typed_type
 
-val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type
+val execute_rec_type : env -> 'a evar_map -> constr -> typed_type