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.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'parsing/ppextend.ml')

diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index aab385a707..b64c2b956a 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -36,9 +36,11 @@ let ppcmd_of_cut = function
   | PpFnl -> fnl ()
   | PpBrk(n1,n2) -> brk(n1,n2)
 
+type pattern_quote_style = QuotedPattern | NotQuotedPattern
+
 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
@@ -50,7 +52,7 @@ type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
   | UnpMetaVar (p1,s1), UnpMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
-  | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpBinderMetaVar (p1,s1), UnpBinderMetaVar (p2,s2) -> entry_relative_level_eq p1 p2 && s1 = s2
   | UnpListMetaVar (p1,l1,s1), UnpListMetaVar (p2,l2,s2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2 && s1 = s2
   | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
-- 
cgit v1.2.3