aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-30 02:39:46 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-11-30 02:39:46 +0100
commit8812851441f13aca6c7f7b1304e8a90ca105245e (patch)
treed3b2ddf76273225532811d16ccde0457b47c4e8b /printing
parent4586e904f8d2759c4f19e1ac3ad5c0447b353ae0 (diff)
Fixing printing of dirpathes in Ppconstr. It was reversed.
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2d0e4e47d..0c687a18e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -154,7 +154,7 @@ end) = struct
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
let id = tag_ref (str (Id.to_string id)) in
- let sl = match DirPath.repr sl with
+ let sl = match List.rev (DirPath.repr sl) with
| [] -> mt ()
| sl ->
let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in