aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 0b5009e26..d16c9bb80 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -214,7 +214,7 @@ type proof_expr =
type syntax_modifier =
| SetItemLevel of string list * Extend.production_level
- | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level
+ | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
| SetLevel of int
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key