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 /printing/prettyp.mli | |
| 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 'printing/prettyp.mli')
| -rw-r--r-- | printing/prettyp.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli index bc0ce1718..de34131fe 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -53,7 +53,9 @@ val print_all_instances : unit -> std_ppcmds val inspect : int -> std_ppcmds (** Locate *) + val print_located_qualid : reference -> std_ppcmds +val print_located_term : reference -> std_ppcmds val print_located_tactic : reference -> std_ppcmds type object_pr = { |