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.
---
 pretyping/patternops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/patternops.mli')

diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 3a1faf1c7..ffe0186af 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -12,6 +12,7 @@ open Glob_term
 open Mod_subst
 open Misctypes
 open Pattern
+open Ltac_pretype
 
 (** {5 Functions on patterns} *)
 
-- 
cgit v1.2.3