diff options
| author | Emilio Jesus Gallego Arias | 2020-02-23 15:42:51 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-23 15:42:51 -0500 |
| commit | b04f8948b167ef227372eeffe299462b6bde1f1b (patch) | |
| tree | a5fbba65180fdf8d9a1ae6a7a9a16f99159328c1 | |
| parent | c4259da61f63ff6c2b088398a6f7fae31a2ebeb2 (diff) | |
| parent | e715ae132c84960f766d64e7a17eea74924eadab (diff) | |
Merge PR #11660: Fix #11654: syntax of inductive declaration.
Reviewed-by: ejgallego
| -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; "}" -> |