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 +---
 pretyping/pretyping.ml  | 1 -
 pretyping/pretyping.mli | 4 +---
 3 files changed, 2 insertions(+), 7 deletions(-)

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 :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3fae20bcb9..32daa0d892 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,6 @@ open Misctypes
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type pure_open_constr = evar_map * EConstr.constr
 
 (************************************************************************)
 (* This concerns Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 1bde4b44ce..002e84a49a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,8 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type pure_open_constr = evar_map * constr
-
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
@@ -77,7 +75,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref ->
 
 val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
-  typing_constraint -> glob_constr -> pure_open_constr
+  typing_constraint -> glob_constr -> evar_map * EConstr.t
 
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
-- 
cgit v1.2.3