diff options
| author | Gaëtan Gilbert | 2019-05-09 14:57:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-09 14:57:28 +0200 |
| commit | a424f7aebaf18935ecf9b897db3cd9829010632f (patch) | |
| tree | 969be39526738aceef400ce634dbf7dc3dd7162f /engine/termops.mli | |
| parent | b2826206063c1ce596736a1e92550b4c24eaea71 (diff) | |
| parent | 66df9050edb8c1fe10992a58f2ec51957cf03449 (diff) | |
Merge PR #10126: Ignore generated dune file for Ltac2
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine/termops.mli')
0 files changed, 0 insertions, 0 deletions