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 /interp/interp.mllib | |
| 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 'interp/interp.mllib')
| -rw-r--r-- | interp/interp.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index 52978a2ab6..33573edcce 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -17,4 +17,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Declare |