From 68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:00:07 +0100
Subject: Merging glob_binder and glob_decl.

---
 interp/constrintern.mli | 2 +-
 intf/glob_term.mli      | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 021b565c8f..d99747be56 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,7 +88,7 @@ val intern_gen : typing_constraint -> env ->
 val intern_pattern : env -> cases_pattern_expr ->
   Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
+val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index f83ff97b21..b3159c860c 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -78,8 +78,6 @@ and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr)
     of [t] are members of [il]. *)
 and cases_clauses = cases_clause list
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
-
 (** A globalised term together with a closure representing the value
     of its free variables. Intended for use when these variables are taken
     from the Ltac environment. *)
-- 
cgit v1.2.3