diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:18:52 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:48:13 +0200 |
commit | eb87cdaeb252d758b6a76b36867254823169576b (patch) | |
tree | 2b1345ba106bd75c6c889524d616ef1062b20237 /theories/ZArith/ZArith_dec.v | |
parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) |
A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).
More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.
(Not to be pushed to v8.6 which has a better fix).
Diffstat (limited to 'theories/ZArith/ZArith_dec.v')
0 files changed, 0 insertions, 0 deletions