diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 22:04:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-03 13:52:04 +0200 |
| commit | e11068aa90f6e7fc728d4583998cd99cfa850211 (patch) | |
| tree | 98998fecef98931fea26e5de7d2156c4a6711d42 /pretyping/globEnv.mli | |
| parent | f19d24a462d50c701a3882de2c16180bb739e622 (diff) | |
[pretyper] Remove imperative passing of evar_map.
Diffstat (limited to 'pretyping/globEnv.mli')
| -rw-r--r-- | pretyping/globEnv.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 70a7ee6e2f..e8a2fbdd16 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -53,10 +53,10 @@ val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t arra (** Declare an evar using renaming information *) -val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> - ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr +val new_evar : t -> evar_map -> ?src:Evar_kinds.t Loc.located -> + ?naming:Namegen.intro_pattern_naming_expr -> constr -> evar_map * constr -val e_new_type_evar : t -> evar_map ref -> src:Evar_kinds.t Loc.located -> constr +val new_type_evar : t -> evar_map -> src:Evar_kinds.t Loc.located -> evar_map * constr (** [hide_variable env na id] tells to hide the binding of [id] in the ltac environment part of [env] and to additionally rebind @@ -73,8 +73,8 @@ val hide_variable : t -> Name.t -> Id.t -> t (** In case a variable is not bound by a term binder, look if it has an interpretation as a term in the ltac_var_map *) -val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) -> - t -> evar_map -> Id.t -> unsafe_judgment +val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> evar_map * unsafe_judgment) -> + t -> evar_map -> Id.t -> evar_map * unsafe_judgment (** Interp an identifier as an ltac variable bound to an identifier, or as the identifier itself if not bound to an ltac variable *) |