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".
---
 plugins/ssrsearch/g_search.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 54fdea0860..2daecd4af8 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -141,7 +141,7 @@ let interp_search_notation ?loc tag okey =
   let rec sub () = function
   | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
-    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x, Explicit) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
   Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
 
-- 
cgit v1.2.3


From 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2020 13:18:09 +0200
Subject: A step towards supporting pattern cast deeplier.

We at least support a cast at the top of patterns in notations.
---
 plugins/ssrsearch/g_search.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 2daecd4af8..74535a10d3 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -141,7 +141,7 @@ let interp_search_notation ?loc tag okey =
   let rec sub () = function
   | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
-    glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x, Explicit) sub () c in
+    glob_constr_of_notation_constr_with_binders ?loc (fun _ x t -> (), None, x, Explicit, t) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
   Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat)
 
-- 
cgit v1.2.3