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 d2cb788ea..69ea84158 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -42,7 +42,7 @@ val new_instance :
?global:bool -> (** Not global by default. *)
?refine:bool -> (** Allow refinement *)
Decl_kinds.polymorphic ->
- local_binder list ->
+ local_binder_expr list ->
typeclass_constraint ->
(bool * constr_expr) option ->
?generalize:bool ->
@@ -63,4 +63,4 @@ val id_of_class : typeclass -> Id.t
(** returns [false] if, for lack of section, it declares an assumption
(unless in a module type). *)
-val context : Decl_kinds.polymorphic -> local_binder list -> bool
+val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool