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.

---
 API/API.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index a0e77edd12..f7cc7ced36 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4008,7 +4008,6 @@ sig
     }
 
   type pure_open_constr = Evd.evar_map * EConstr.constr
-  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
 
   val understand_ltac : inference_flags ->
                         Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
@@ -4387,8 +4386,10 @@ end
 
 module Evar_refiner :
 sig
+  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
+
   val w_refine : Evar.t * Evd.evar_info ->
-                 Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
+                 glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
 end
 
 
-- 
cgit v1.2.3