diff options
| author | Pierre-Marie Pédrot | 2019-06-21 00:16:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 10:59:12 +0200 |
| commit | 2720db38d74e3e8d26077ad03d79221f0734465c (patch) | |
| tree | 98daf5f97f01e9f6cdb36ff7fb474c07a0ded78e /kernel/term_typing.ml | |
| parent | ee1717a5ac72373acddf1bbe913eebe8943f3c18 (diff) | |
Move Declare to tactics folder.
Nobody really knows where this module should belong, it seems. My personal
theory is that it should live in vernac instead, but due to nasty
interactions with abstract-like tactics, we have to put it somewhere below.
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions