From 52b93b587b9cb53b0ed11c7d6cf5f328d7ee1479 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 23 Oct 2020 22:58:30 +0200
Subject: Add preliminary support for notations with large class
 (non-recursive) binders.

We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
---
 parsing/ppextend.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'parsing/ppextend.mli')

diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 56a3fc8e3c..ca22aacacf 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -28,10 +28,12 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** {6 Printing rules for notations} *)
 
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
   | UnpMetaVar of entry_relative_level * Extend.side option
-  | UnpBinderMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level * pattern_quote_style
   | UnpListMetaVar of entry_relative_level * unparsing list * Extend.side option
   | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
-- 
cgit v1.2.3