diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:05:44 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 15:05:44 +0200 |
| commit | 3af594bb07b3faf8d766bb1e9b6bead7cb1081d8 (patch) | |
| tree | 578cd62b6200a386de57c9bdcf41676c0a9009fd /plugins/ltac/pptactic.ml | |
| parent | 3fd0490c113432ae3fea6e6defa7b79acb36eae6 (diff) | |
| parent | b789106117653fec8340ecbd88866c254fe1201d (diff) | |
Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70ea9c.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
0 files changed, 0 insertions, 0 deletions