diff options
| author | Yann Régis-Gianas | 2014-11-05 22:52:09 +0100 |
|---|---|---|
| committer | Yann Régis-Gianas | 2014-11-05 22:52:24 +0100 |
| commit | 6b69fc07f9f17e4d61dbb244c69f6c9de326e00f (patch) | |
| tree | fde7d3a055c7c8366504ea18913a816fb6dc325e /printing/pptactic.ml | |
| parent | 3d2b9f1329557dd54720718bf064010d9538ea03 (diff) | |
lib/RichPp: Rename into Richpp.
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ad3f95ef24..44f4b456cc 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1339,14 +1339,14 @@ let _ = Hook.set Tactic_debug.match_rule_printer pr_match_rule false (pr_glob_tactic (Global.env())) (fun (_,p) -> pr_constr_pattern p) rl) -module RichPp (Indexer : sig +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) = struct - include Make (Ppconstr.RichPp (Indexer)) (struct + include Make (Ppconstr.Richpp (Indexer)) (struct open Ppannotation open Indexer - let tag_keyword = Pp.tag (Indexer.index AKeyword) + let tag_keyword = Pp.tag (Indexer.index AKeyword) let tag_glob_tactic_expr e = Pp.tag (index (AGlobTacticExpr e)) let tag_glob_atomic_tactic_expr a = Pp.tag (index (AGlobAtomicTacticExpr a)) let tag_raw_tactic_expr e = Pp.tag (index (ARawTacticExpr e)) |