diff options
39 files changed, 238 insertions, 238 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 diff --git a/library/declare.ml b/library/declare.ml index 0dcdf3dd2..9a32c1d46 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 0fc1852cb..5cefe53f6 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 3e557b350..a61b09c58 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 8fe93b97c..2cc34c3cb 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 da2ae3102..f1d1b5190 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 dd1f32bd1..7cc35efca 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) -> diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 7c48d2818..9ea2929ed 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -38,18 +38,18 @@ val globalize_ast : Coqast.t -> Coqast.t (*i Ceci était avant dans Trad Maintenant elles sont là car relève des ast i*) -val type_of_com : unsafe_env -> Coqast.t -> typed_type +val type_of_com : env -> Coqast.t -> typed_type val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr -> constr -val constr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr -val constr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr -val constr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr +val constr_of_com1 : bool -> 'c evar_map -> env -> Coqast.t -> constr +val constr_of_com : 'c evar_map -> env -> Coqast.t -> constr +val constr_of_com_sort : 'c evar_map -> env -> Coqast.t -> constr -val fconstr_of_com1 : bool -> 'c evar_map -> unsafe_env -> Coqast.t -> constr -val fconstr_of_com : 'c evar_map -> unsafe_env -> Coqast.t -> constr -val fconstr_of_com_sort : 'c evar_map -> unsafe_env -> Coqast.t -> constr +val fconstr_of_com1 : bool -> 'c evar_map -> env -> Coqast.t -> constr +val fconstr_of_com : 'c evar_map -> env -> Coqast.t -> constr +val fconstr_of_com_sort : 'c evar_map -> env -> Coqast.t -> constr (* Typing with Trad, and re-checking with Mach *) diff --git a/parsing/pretty.mli b/parsing/pretty.mli index dd8d605ed..0691f0a01 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -27,10 +27,10 @@ val print_full_context_typ : unit -> std_ppcmds val print_crible : identifier -> unit val print_sec_context : string -> std_ppcmds val print_sec_context_typ : string -> std_ppcmds -val print_val : unsafe_env -> unsafe_judgment -> std_ppcmds -val print_type : unsafe_env -> unsafe_judgment -> std_ppcmds +val print_val : env -> unsafe_judgment -> std_ppcmds +val print_type : env -> unsafe_judgment -> std_ppcmds val print_eval : - 'a reduction_function -> unsafe_env -> unsafe_judgment -> std_ppcmds + 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds val implicit_args_msg : section_path -> mutual_inductive_packet array -> std_ppcmds val print_mutual : section_path -> mutual_inductive_body -> std_ppcmds diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 25163f6e6..8c2f84887 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 3fc8dfb91..c510299ac 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 59dfc7895..9310e5dd3 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 3cbf887c5..501e9f28e 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 68e68c1b4..c0997c044 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 4e37b18a7..33238ecd9 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 84097f858..995779783 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 e49171a2a..8304434d8 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 b12cd369d..80fcc5ec9 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 diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 0f121a9f2..47bba83fa 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 f89c6e9b4..a3e387b6e 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 ee0f3de89..067162e60 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 3801f9e4b..7b612ac5f 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 ea13c75a7..be9761efd 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 ccaaae4fb..a1aec82cd 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 diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bd66561dd..6fb962f2c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -265,7 +265,7 @@ let case_sign ity i = | [] -> acc | (c::rest) -> analrec (false::acc) rest in - let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in + let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in analrec [] recarg.(i-1) let elim_sign ity i = @@ -277,7 +277,7 @@ let elim_sign ity i = | (Mrec k::rest) -> analrec ((j=k)::acc) rest | [] -> List.rev acc in - let recarg = mis_recarg (lookup_mind_specif ity (Global.unsafe_env())) in + let recarg = mis_recarg (lookup_mind_specif ity (Global.env())) in analrec [] recarg.(i-1) let sort_of_goal gl = diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index e541c29db..50425b002 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -82,7 +82,7 @@ let clenv_constrain_with_bindings bl clause = [< 'sTR"Clause did not have " ; 'iNT n ; 'sTR"-th" ; 'sTR" absolute argument" >]) in - let env = Global.unsafe_env () in + let env = Global.env () in let sigma = Evd.empty in let k_typ = nf_betaiota env sigma (clenv_instance_type clause k) in let c_typ = nf_betaiota env sigma (w_type_of clause.hook c) in @@ -141,7 +141,7 @@ let rec build_args acc ce p_0 p_1 = | (_, (_::_)) -> failwith "mk_clenv_using" and build_term ce p_0 p_1 = - let env = Global.unsafe_env() in + let env = Global.env() in match p_0,p_1 with | ((na,Some t), (DOP0(Meta mv))) -> build_term ce (na,Some t) mkExistential @@ -196,7 +196,7 @@ let clenv_apply_n_times n ce = let templtyp = clenv_instance_template_type ce and templval = (clenv_template ce).rebus in let rec apprec ce argacc (n,ty) = - let env = Global.unsafe_env () in + let env = Global.env () in match (n, whd_betadeltaiota env (w_Underlying ce.hook) ty) with | (0, templtyp) -> clenv_change_head (applist(templval,List.rev argacc), templtyp) ce |