diff options
| author | herbelin | 2010-06-03 22:33:36 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-03 22:33:36 +0000 |
| commit | 238309bfddfa68f7a4982afa6a005a8110b0ffb1 (patch) | |
| tree | 814866575d8236971377f7f07ef18a23335fb99b /toplevel | |
| parent | e75806ead6c7a45f804b057df90b2bc98b50259d (diff) | |
Added command "Locate Ltac qid".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13067 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 11 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6cf215ec2..0ed1186a05 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -254,6 +254,15 @@ let print_located_module r = str "No module is referred to by name ") ++ pr_qualid qid in msgnl msg +let print_located_tactic r = + let (loc,qid) = qualid_of_reference r in + msgnl + (try + str "Ltac " ++ + pr_path (Nametab.path_of_tactic (Nametab.locate_tactic qid)) + with Not_found -> + str "No Ltac definition is referred to by " ++ pr_qualid qid) + let smart_global r = let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr; @@ -1145,6 +1154,7 @@ let vernac_locate = function (Constrextern.without_symbols pr_lrawconstr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> print_located_module qid + | LocateTactic qid -> print_located_tactic qid | LocateFile f -> locate_file f (********************) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ebdec85eec..bb35445ce2 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -78,6 +78,7 @@ type locatable = | LocateTerm of reference or_by_notation | LocateLibrary of reference | LocateModule of reference + | LocateTactic of reference | LocateFile of string type goable = |