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.
---
 interp/notation_ops.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c8fcbf7410..a61ba172ee 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,12 +47,9 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
 exception No_match
 
-type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
-      glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
-      (glob_decl2 list * subscopes) list
+      (extended_glob_local_binder list * subscopes) list
 
 val match_notation_constr_cases_pattern :
   cases_pattern -> interpretation ->
-- 
cgit v1.2.3