diff options
| author | Théo Zimmermann | 2020-02-23 11:08:56 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-23 11:08:56 +0100 |
| commit | e715ae132c84960f766d64e7a17eea74924eadab (patch) | |
| tree | f1aa1d2296a30352ff9c33467f708bb0925516f5 | |
| parent | 8e3ff397ed403f3da90300ec3196810167ce61a0 (diff) | |
Fix #11654: syntax of inductive declaration.
Inductive foo := Bar |. was accepted but it shouldn't have.
| -rw-r--r-- | vernac/g_vernac.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d597707d12..def4ed942a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,7 +402,7 @@ GRAMMAR EXTEND Gram ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { Constructors ((c id)::l) } | id = identref ; c = constructor_type -> { Constructors [ c id ] } | cstr = identref; "{"; fs = record_fields; "}" -> |