diff options
| author | Pierre-Marie Pédrot | 2014-07-21 15:59:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-21 16:44:30 +0200 |
| commit | f27df397b49d2bb469e513749cade21e5c259926 (patch) | |
| tree | 995eefeb3129ce9bb773597bf2c2548793350eb5 /parsing | |
| parent | 32ea597251d4fc7cfbab26022a5355949e8a3257 (diff) | |
Adding a new "Locate Term" command, distinct from the raw "Locate" command.
The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".
Fixes bug #3380.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5f49a318d4..0b6fc7bf78 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -908,7 +908,8 @@ GEXTEND Gram | qid = smart_global -> RefClass qid ] ] ; locatable: - [ [ qid = smart_global -> LocateTerm qid + [ [ qid = smart_global -> LocateAny qid + | IDENT "Term"; qid = smart_global -> LocateTerm qid | IDENT "File"; f = ne_string -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid | IDENT "Module"; qid = global -> LocateModule qid |