diff options
| author | coqbot-app[bot] | 2020-11-20 22:01:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 22:01:06 +0000 |
| commit | 23d30fa1c19af9a29787204d81d7bd2d2e0c9b1f (patch) | |
| tree | 98e1452ac1c2b2e88178461fbe51393d1d918f3e /plugins | |
| parent | 87a59a875b0945fa7976fd16b17a2ff5dd015402 (diff) | |
| parent | 345bcc504a1ed4f11d328cc1dfa17ba37f6875b3 (diff) | |
Merge PR #13265: Add support for general non-necessarily-recursive binders in notations
Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg index 54fdea0860..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) 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) |