diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 48a7a7a5a8..bcb2f7a576 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -615,11 +615,12 @@ GEXTEND Gram | IDENT "SearchAbout"; sl = [ "["; l = LIST1 [ - b = positive_search_mark; r = global -> b,SearchRef r - | b = positive_search_mark; s = ne_string; sc = OPT scope - -> b,SearchString (s,sc) + b = positive_search_mark; s = ne_string; sc = OPT scope + -> b, SearchString (s,sc) + | b = positive_search_mark; p = constr_pattern + -> b, SearchSubPattern p ]; "]" -> l - | qid = global -> [true,SearchRef qid] + | p = constr_pattern -> [true,SearchSubPattern p] | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ]; l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) |