diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 09:49:37 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 09:49:37 +0200 |
| commit | 00aa9287eb73ce9f3b41444ed23bc370cde828aa (patch) | |
| tree | f32a276ba6bcb9fbf8ca560567b44f8d86a7e3bd /vernac/metasyntax.ml | |
| parent | 836e0df2ee3cec97adcadd70be218d9c57bbc313 (diff) | |
| parent | 9bc2b3d6d0f7d02843180bca5a4d1f908e8a6141 (diff) | |
Merge PR #1060: An optimization of tactic constructor
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions