From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 24 Oct 2017 14:35:25 +0200
Subject: [general] Remove Econstr dependency from `intf`

To this extent we factor out the relevant bits to a new file,
ltac_pretype.
---
 interp/constrextern.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 593580fb7..b2df449c5 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -19,6 +19,7 @@ open Constrexpr
 open Notation_term
 open Notation
 open Misctypes
+open Ltac_pretype
 
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
-- 
cgit v1.2.3