diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-19 10:41:40 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-19 10:41:40 +0200 |
| commit | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (patch) | |
| tree | 4a58470178b2f18952473db9ccfee393aa8b3af9 /vernac/topfmt.ml | |
| parent | e5ee848ac9180b7074b97f87c4ba057241f2979e (diff) | |
| parent | 12d6d60dc10654b60a31dc5bdca765409dd4898f (diff) | |
Merge PR#573: [toplevel] Fix printing of parsing errors + corner case.
Diffstat (limited to 'vernac/topfmt.ml')
0 files changed, 0 insertions, 0 deletions