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 /lib | |
| 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 'lib')
| -rw-r--r-- | lib/clib.mllib | 2 | ||||
| -rw-r--r-- | lib/richpp.ml (renamed from lib/richPp.ml) | 0 | ||||
| -rw-r--r-- | lib/richpp.mli (renamed from lib/richPp.mli) | 0 |
3 files changed, 1 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib index 568ffbe0ef..3fee888543 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -32,7 +32,7 @@ Pp Xml_lexer Xml_parser Xml_printer -RichPp +Richpp CUnix Envars Aux_file diff --git a/lib/richPp.ml b/lib/richpp.ml index f9a7e83a8e..f9a7e83a8e 100644 --- a/lib/richPp.ml +++ b/lib/richpp.ml diff --git a/lib/richPp.mli b/lib/richpp.mli index 834115d40b..834115d40b 100644 --- a/lib/richPp.mli +++ b/lib/richpp.mli |