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 /dev | |
| parent | 8e3ff397ed403f3da90300ec3196810167ce61a0 (diff) | |
Fix #11654: syntax of inductive declaration.
Inductive foo := Bar |. was accepted but it shouldn't have.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions