X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.ml;h=c15b6fe7144bf6f43bba96aabd22ef434ace8980;hb=206f96afb7097c20b3cc8bd144825467b4fde7ae;hp=6af1efd714406afea6c87e2bf0d37af966b402ae;hpb=cb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 6af1efd71..c15b6fe71 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -261,6 +261,11 @@ let pp_associativity = function
 
 let pp_precedence i = sprintf "with precedence %d" i
 
+let pp_dir_opt = function
+  | None -> ""
+  | Some `LeftToRight -> "> "
+  | Some `RightToLeft -> "< "
+
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
@@ -277,8 +282,9 @@ let pp_command = function
         dsc symbol
         (String.concat " " (List.map pp_argument_pattern arg_patterns))
         (pp_cic_appl_pattern cic_appl_pattern)
-  | Notation (_, l1_pattern, assoc, prec, l2_pattern) ->
-      sprintf "notation \"%s\" %s %s for %s"
+  | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+      sprintf "notation %s\"%s\" %s %s for %s"
+        (pp_dir_opt dir_opt)
         (pp_l1_pattern l1_pattern)
         (pp_associativity assoc)
         (pp_precedence prec)