From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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.
---
 proofs/evar_refiner.ml  | 1 +
 proofs/evar_refiner.mli | 1 +
 proofs/tacmach.mli      | 1 +
 3 files changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 48fa2202ee..d38ff7512f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -14,6 +14,7 @@ open Evarutil
 open Evarsolve
 open Pp
 open Glob_term
+open Ltac_pretype
 
 (******************************************)
 (* Instantiation of existential variables *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 5d69715967..a0e3b718a2 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -8,6 +8,7 @@
 
 open Evd
 open Glob_term
+open Ltac_pretype
 
 (** Refinement of existential variables. *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7e6d83b10f..d4e9555f34 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,6 +15,7 @@ open Proof_type
 open Redexpr
 open Pattern
 open Locus
+open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
-- 
cgit v1.2.3