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 119ff5222..d87a19d28 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -61,7 +61,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> (** Recursor names utilities *) -val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t val elimination_suffix : Sorts.family -> string val make_elimination_ident : Id.t -> Sorts.family -> Id.t |