diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:47:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:47:47 +0100 |
| commit | 9122b9244ed0907ce91b50bbe3584d69cb340baa (patch) | |
| tree | 2cdfa907b1e1fb08f48520aa7682d21e6372e539 /lib/loc.mli | |
| parent | 7b14d01ccc41b47df9644391bf01e4b7949e571d (diff) | |
| parent | b80f10a95692c3e4fd95f5ed196311e22fc044b4 (diff) | |
Merge PR #6900: [compat] Remove "Tactic Pattern Unification"
Diffstat (limited to 'lib/loc.mli')
0 files changed, 0 insertions, 0 deletions