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/API.mli')

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


From cd0a6070d9627cdf335c4be0a03b9bbb81f7a738 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Sep 2016 16:53:23 +0200
Subject: Remove pure_open_constr (now open_constr)

---
 API/API.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index f7cc7ced36..9dc78cbe47 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4007,11 +4007,9 @@ sig
       expand_evars : bool
     }
 
-  type pure_open_constr = Evd.evar_map * EConstr.constr
-
   val understand_ltac : inference_flags ->
                         Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
-                        typing_constraint -> Glob_term.glob_constr -> pure_open_constr
+                        typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
   val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                        ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
   val type_uconstr :
-- 
cgit v1.2.3


From a92b0e3abb476743f6f12ce828a0d82eb3c98e98 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Sep 2016 17:31:51 +0200
Subject: Move type_uconstr to Tacinterp.

---
 API/API.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 9dc78cbe47..f4a7be2a3f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4012,10 +4012,6 @@ sig
                         typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
   val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                        ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
-  val type_uconstr :
-    ?flags:inference_flags ->
-    ?expected_type:typing_constraint ->
-    Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
   val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
                    Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context
   val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
-- 
cgit v1.2.3