From 2720db38d74e3e8d26077ad03d79221f0734465c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Jun 2019 00:16:10 +0200
Subject: 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.
---
 interp/interp.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/interp.mllib')

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
-- 
cgit v1.2.3