diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-25 16:08:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-21 17:54:13 +0200 |
| commit | 2d9630171c6e17e85eb9c1b51a59fa381716380a (patch) | |
| tree | 3b5c4bf90218b4e01adc55be6c288d342f120f21 /grammar | |
| parent | d6eb4a26648817f6b034e95c02622cadf0fa65ca (diff) | |
Fix an anomaly when calling Obligation 0 or Obligation -1.
I didn't change the parser which expects an integer instead of a positive number
because changing it would also mean having worse error messages because of our
current LL parser. The error message would have been:
Syntax error: 'Tactic' ':=' expected after 'Obligation' (in
[vernac:command]).
Diffstat (limited to 'grammar')
0 files changed, 0 insertions, 0 deletions