From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 15 Sep 2016 18:11:54 +0200
Subject: Untangling Tacexpr from lower strata.

---
 tactics/equality.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.mli')

diff --git a/tactics/equality.mli b/tactics/equality.mli
index 47cb6b82f..6a4a8126e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,10 +11,10 @@ open Names
 open Term
 open Evd
 open Environ
-open Tacexpr
 open Ind_tables
 open Locus
 open Misctypes
+open Tactypes
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
-- 
cgit v1.2.3