From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 12:35:56 +0200
Subject: Respecting the ident/pattern distinction in notation modifiers.

---
 intf/notation_term.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 83cc454f43..0f4bfef600 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -60,8 +60,11 @@ type subscopes = tmp_scope_name option * scope_name list
 
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
+
+type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern
+
 type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList
+  | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
 
 (** Type of variables when interpreting a constr_expr as a notation_constr:
     in a recursive pattern x..y, both x and y carry the individual type
-- 
cgit v1.2.3