diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:05:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-09 15:05:56 +0200 |
| commit | c3f7302e9f6849298bbb34dc91516751444888ff (patch) | |
| tree | 0a409a093848f0e26c876d4023132bcf885e7259 /vernac/metasyntax.ml | |
| parent | f1598b00219a951e94036cb7f48a8fe1309025f1 (diff) | |
| parent | c04536a44bd55d6ddef3ed4f3bf2c3a1dd3bb258 (diff) | |
Merge PR #1117: [ci] Remove temporary bignums overlay.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions