diff options
Diffstat (limited to 'pretyping/globEnv.mli')
| -rw-r--r-- | pretyping/globEnv.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index e8a2fbdd16..63f72e60bd 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -13,6 +13,7 @@ open Environ open Evd open EConstr open Ltac_pretype +open Evarutil (** To embed constr in glob_constr *) @@ -37,7 +38,7 @@ type t (** Build a pretyping environment from an ltac environment *) -val make : env -> evar_map -> ltac_var_map -> t +val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t (** Export the underlying environement *) @@ -47,9 +48,9 @@ val vars_of_env : t -> Id.Set.t (** Push to the environment, returning the declaration(s) with interpreted names *) -val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t -val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t -val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t +val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t +val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t +val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t (** Declare an evar using renaming information *) |