From ba0975d00f49684e33f763e171f9578a702eec85 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Sep 2016 16:51:19 +0200
Subject: Move glob_constr_ltac_closure to evar_refiner.

---
 proofs/evar_refiner.ml  | 3 +++
 proofs/evar_refiner.mli | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index cc81adb853..48fa2202ee 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -13,11 +13,14 @@ open Evd
 open Evarutil
 open Evarsolve
 open Pp
+open Glob_term
 
 (******************************************)
 (* Instantiation of existential variables *)
 (******************************************)
 
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
 let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
   let t1 = EConstr.of_constr t1 in
   let t2 = EConstr.of_constr t2 in
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b65ffb1bee..5d69715967 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -7,9 +7,11 @@
 (************************************************************************)
 
 open Evd
-open Pretyping
+open Glob_term
 
 (** Refinement of existential variables. *)
 
+type glob_constr_ltac_closure = ltac_var_map * glob_constr
+
 val w_refine : evar * evar_info ->
   glob_constr_ltac_closure -> evar_map -> evar_map
-- 
cgit v1.2.3