aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.mli')
-rw-r--r--vernac/classes.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eea2a211d..bd30b2d60 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
(** Instance declaration *)
-val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
val declare_instance_constant :