aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.mli')
-rw-r--r--vernac/classes.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e6134ee5d..27d3a4669 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -30,7 +30,7 @@ val declare_instance_constant :
hint_info_expr -> (** priority *)
bool -> (** globality *)
Impargs.manual_explicitation list -> (** implicits *)
- ?hook:(Globnames.global_reference -> unit) ->
+ ?hook:(GlobRef.t -> unit) ->
Id.t -> (** name *)
Univdecls.universe_decl ->
bool -> (* polymorphic *)
@@ -50,7 +50,7 @@ val new_instance :
(bool * constr_expr) option ->
?generalize:bool ->
?tac:unit Proofview.tactic ->
- ?hook:(Globnames.global_reference -> unit) ->
+ ?hook:(GlobRef.t -> unit) ->
hint_info_expr ->
Id.t