diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8addcd3ca5..5fff24fef7 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -155,6 +155,7 @@ type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option +type record_kind = Record | Structure | Class type decl_notation = (string * constr_expr * scope_name option) option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list @@ -163,7 +164,7 @@ 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 bool * lident option * local_decl_expr with_coercion with_notation list + | RecordDecl of record_kind * lident option * local_decl_expr with_coercion with_notation list type inductive_expr = lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr @@ -216,7 +217,7 @@ type vernac_expr = | VernacCombinedScheme of lident * lident list (* Gallina extensions *) - | VernacRecord of (bool*bool) (* = Structure or Class * Inductive or CoInductive *) + | VernacRecord of (record_kind*bool) (* = Structure or Class * Inductive or CoInductive *) * lident with_coercion * local_binder list * constr_expr option * lident option * local_decl_expr with_coercion with_notation list | VernacBeginSection of lident |