diff options
| author | herbelin | 2013-04-17 18:33:16 +0000 |
|---|---|---|
| committer | herbelin | 2013-04-17 18:33:16 +0000 |
| commit | 9b24b6d763bb2c7975cd2b93364d7647fd660598 (patch) | |
| tree | bc4733a59179e67274c9c82ac18db28b2e9d4a23 /parsing | |
| parent | 248e7beca97c073d0f5a2f937d77f2c4d8c805df (diff) | |
Renaming SearchAbout into Search and Search into SearchHead.
I hope I did not forget any place to change.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 56abf3e1c4..004dbab7b4 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -766,15 +766,18 @@ GEXTEND Gram | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid) (* Searching the environment *) - | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchHead c, l) | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchPattern c, l) | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchRewrite c, l) + | IDENT "Search"; s = searchabout_query; l = searchabout_queries -> + let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m) + (* compatibility: SearchAbout *) | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl), m) - (* compatibility format of SearchAbout, with "[ ... ]" *) + (* compatibility: SearchAbout with "[ ... ]" *) | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) |