diff options
Diffstat (limited to 'pretyping/indrec.mli')
| -rw-r--r-- | pretyping/indrec.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 1bf5fd90c6..610a7bf39b 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -63,6 +63,6 @@ val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string -val make_elimination_ident : identifier -> sorts_family -> identifier +val make_elimination_ident : Id.t -> sorts_family -> Id.t val case_suffix : string |