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/inv.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/inv.mli')

diff --git a/tactics/inv.mli b/tactics/inv.mli
index af1cb996a..df629e7c9 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Misctypes
-open Tacexpr
+open Tactypes
 
 type inversion_status = Dep of constr option | NoDep
 
-- 
cgit v1.2.3