diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-07 22:20:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-02 20:56:28 +0200 |
| commit | 160e9f8c7d1af2357db4a37d834b0b9bb28632fb (patch) | |
| tree | 49e5f251c2fe8d4ccd27ddd1c74b37cc6003b15c /library | |
| parent | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff) | |
Refuse to parse empty [Context] command.
The error is now:
Syntax error: [constr:binder] expected after 'Context' (in [vernac:gallina_ext]).
Close #7452.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions