diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 15:59:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-21 16:44:30 +0200 |
| commit | f27df397b49d2bb469e513749cade21e5c259926 (patch) | |
| tree | 995eefeb3129ce9bb773597bf2c2548793350eb5 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 737d1c523..4141f9f56 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1532,8 +1532,10 @@ let vernac_search s r = msg_notice (Search.search_about (List.map (on_snd interp_search_about_item) sl) r) let vernac_locate = function - | LocateTerm (AN qid) -> msg_notice (print_located_qualid qid) - | LocateTerm (ByNotation (_,ntn,sc)) -> + | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) + | LocateTerm (AN qid) -> msg_notice (print_located_term qid) + | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *) + | LocateTerm (ByNotation (_, ntn, sc)) -> msg_notice (Notation.locate_notation (Constrextern.without_symbols pr_lglob_constr) ntn sc) |