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.
---
 tactics/tactics.ml  | 2 +-
 tactics/tactics.mli | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e8a78d72d6..6ab6432394 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -839,7 +839,7 @@ let e_change_in_hyp redfun (id,where) =
     (convert_hyp c)
   end
 
-type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
 
 let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e07d514cd0..32923ea811 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -21,6 +21,7 @@ open Unification
 open Misctypes
 open Tactypes
 open Locus
+open Ltac_pretype
 
 (** Main tactics defined in ML. This file is huge and should probably be split
     in more reasonable units at some point. Because of its size and age, the
-- 
cgit v1.2.3