diff options
| author | Gaëtan Gilbert | 2018-10-30 18:07:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 21:47:36 +0100 |
| commit | 9a99bad924f3c82107a5ecfa7a906988f0f69309 (patch) | |
| tree | 53aa873fec4c075ffb8a1134ab466ba2d24764e9 /pretyping/arguments_renaming.mli | |
| parent | a492288930a3f804ad05def938dd572ccf680a66 (diff) | |
Check univ instances in Typing.
Diffstat (limited to 'pretyping/arguments_renaming.mli')
| -rw-r--r-- | pretyping/arguments_renaming.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 6a776dc961..6d1b6eefd4 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -17,6 +17,8 @@ val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit (** [Not_found] is raised if no names are defined for [r] *) val arguments_names : GlobRef.t -> Name.t list +val rename_type : types -> GlobRef.t -> types + val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types val rename_type_of_constructor : env -> pconstructor -> types |