aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-02-02 18:21:51 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 12:17:35 +0100
commit4e4fb7bd42364fd623f8e0e0d3007cd79d78764b (patch)
tree42dfb8c1b0d8db6b3c70da6d093de9b4fec2385c /vernac/classes.mli
parent68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 (diff)
Renaming local_binder into local_binder_expr.
This is a bit long, but it is to keep a symmetry with constr_expr.
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