From 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 20:21:14 +0100
Subject: Using the same type of binders for interning and externing.

Previously a union type was used for externing.

In particular, moving extended_glob_local_binder to glob_constr.ml.
---
 intf/glob_term.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'intf')

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index b3159c860c..ce862cf8a7 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -78,6 +78,11 @@ 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 extended_glob_local_binder =
+  | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr
+  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * 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