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