From 63b530234e0b19323a50c52434a7439518565c81 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 May 2018 03:15:17 +0200
Subject: [notations] Split interpretation and parsing of notations

Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.

We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
---
 parsing/extend.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 734b859f60..f2af594ef4 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -31,11 +31,6 @@ type production_level =
   | NextLevel
   | NumLevel of int
 
-type constr_as_binder_kind =
-  | AsIdent
-  | AsIdentOrPattern
-  | AsStrictPattern
-
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
@@ -44,7 +39,7 @@ type 'a constr_entry_key_gen =
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of 'a
-  | ETConstrAsBinder of constr_as_binder_kind * 'a
+  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
   | ETOther of string * string
 
-- 
cgit v1.2.3