diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ca539f28a..2727100bf 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -159,12 +159,13 @@ type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a +type 'a with_notation = 'a * decl_notation type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_coercion list + | RecordDecl of lident option * local_decl_expr with_coercion with_notation list type inductive_expr = - lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr + lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr type module_binder = bool option * lident list * module_type_ast @@ -217,7 +218,7 @@ type vernac_expr = (* Gallina extensions *) | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *) * lident with_coercion * local_binder list - * constr_expr * lident option * local_decl_expr with_coercion list + * constr_expr * lident option * local_decl_expr with_coercion with_notation list | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of |