diff options
author | 2014-11-05 22:52:09 +0100 | |
---|---|---|
committer | 2014-11-05 22:52:24 +0100 | |
commit | 6b69fc07f9f17e4d61dbb244c69f6c9de326e00f (patch) | |
tree | fde7d3a055c7c8366504ea18913a816fb6dc325e /printing/ppvernac.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/ppvernac.ml')
-rw-r--r-- | printing/ppvernac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8814daf70..21fac8a35 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1272,13 +1272,13 @@ include Make (Ppconstr) (Pptactic) (struct let tag_vernac = do_not_tag end) -module RichPp (Indexer : sig +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) = struct include Make - (Ppconstr.RichPp (Indexer)) - (Pptactic.RichPp (Indexer)) + (Ppconstr.Richpp (Indexer)) + (Pptactic.Richpp (Indexer)) (struct open Ppannotation let tag_keyword = Pp.tag (Indexer.index AKeyword) |