diff options
| author | Hugo Herbelin | 2018-04-13 18:01:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | bb78a36d77ff37ba9fc11d6db914ee4bc71e3e2e (patch) | |
| tree | 744607c59fa472a2de30e9bf41f90807a10f2790 /pretyping/globEnv.mli | |
| parent | 9371ab87e8bac42216f882ed8f00e6fba9dc6eb0 (diff) | |
Relying on the precomputation of the renaming also for new_evar_type.
Diffstat (limited to 'pretyping/globEnv.mli')
| -rw-r--r-- | pretyping/globEnv.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 2d67e25dcd..4038523211 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -56,6 +56,8 @@ val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t arra val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr +val e_new_type_evar : t -> evar_map ref -> src:Evar_kinds.t Loc.located -> constr + (** [hide_variable env na id] tells to hide the binding of [id] in the ltac environment part of [env] and to additionally rebind it to [id'] in case [na] is some [Name id']. It is useful e.g. |