diff options
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 67078ab23..778aef105 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -103,9 +103,9 @@ GEXTEND Gram | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchRewrite c, l) | IDENT "SearchAbout"; - sl = [ "["; l = LIST1 [ r = global -> Search.SearchRef r - | s = STRING -> Search.SearchString s ]; "]" -> l - | qid = global -> [Search.SearchRef qid] ]; + sl = [ "["; l = LIST1 [ r = global -> SearchRef r + | s = STRING -> SearchString s ]; "]" -> l + | qid = global -> [SearchRef qid] ]; l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> |