diff options
| author | Théo Zimmermann | 2018-12-11 10:00:30 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-11 10:00:30 +0100 |
| commit | 97f5f37f782ffb9914fa8f67e745ba1effad20be (patch) | |
| tree | 3f673b9ffb341759177ca0754ee568b550819b42 /tactics/redexpr.mli | |
| parent | 10b07a187522b74bbcc9355d3ff9c4153f300706 (diff) | |
| parent | 6aba0471154d68bbd40a512f741a10f32948d80f (diff) | |
Merge PR #9151: [dune] Teach coq_dune about `.glob` and `.aux` files.
Diffstat (limited to 'tactics/redexpr.mli')
0 files changed, 0 insertions, 0 deletions