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.

---
 intf/glob_term.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

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