diff options
| author |  Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-05 22:52:09 +0100 |
|---|---|---|
| committer | Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-05 22:52:24 +0100 |
| commit | 6b69fc07f9f17e4d61dbb244c69f6c9de326e00f (patch) | |
| tree | fde7d3a055c7c8366504ea18913a816fb6dc325e /printing/ppvernac.mli | |
| 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.mli')
| -rw-r--r-- | printing/ppvernac.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 616fc7345..06f51f060 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -20,5 +20,5 @@ include Ppvernacsig.Pp Please refer to {!RichPp} to know what are the requirements over [Indexer.index] behavior. *) -module RichPp (Indexer : sig val index : Ppannotation.t -> string end) +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) : Ppvernacsig.Pp |