aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 6f6cff275..2525c430a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,11 +163,9 @@ module Constr :
val constr_pattern : constr_expr Gram.Entry.e
val lconstr_pattern : constr_expr Gram.Entry.e
val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
- val binder_let : local_binder Gram.Entry.e
- val delimited_binder_let : local_binder Gram.Entry.e
+ val binder_let : local_binder list Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
- val delimited_binders_let : local_binder list Gram.Entry.e
val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
end