diff options
| author | Maxime Dénès | 2017-10-09 15:38:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 15:38:20 +0200 |
| commit | 81753dcda29bf7d7ecd6c8c0ddb3347f4cd49766 (patch) | |
| tree | 8af2a8e24a87fb5dea0bb6dc2feadd6b0e06fd3b /printing/ppvernac.ml | |
| parent | d5534aab708e5d3bd6c3633dc9d028016eeb3076 (diff) | |
| parent | 347d94a4b966d0cc4a3a04814b0c76c4b05caa11 (diff) | |
Merge PR #1114: Generic handling of nameable objects for plugins
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 10dd42ea91..a1cdfdbaa2 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1156,7 +1156,7 @@ open Decl_kinds | LocateFile f -> keyword "File" ++ spc() ++ qs f | LocateLibrary qid -> keyword "Library" ++ spc () ++ pr_module qid | LocateModule qid -> keyword "Module" ++ spc () ++ pr_module qid - | LocateTactic qid -> keyword "Ltac" ++ spc () ++ pr_ltac_ref qid + | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid in return (keyword "Locate" ++ spc() ++ pr_locate loc) | VernacRegister (id, RegisterInline) -> |