X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.ml;h=7d1f8c22e843e53a5c942851e897c35f2be6d083;hb=95977594b05ba0320784a445d480b3fe11ef4e55;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..7d1f8c22e 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -39,10 +39,12 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms)
 
 let pp_reduction_kind = function
+  | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
+  | `Unfold (Some t) -> "unfold " ^ pp_term_ast t
+  | `Unfold None -> "unfold"
   | `Whd -> "whd"
-  | `Normalize -> "normalize"
  
   
 let pp_pattern (t, hyp, goal) = 
@@ -261,6 +263,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 +284,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)