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