X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=45fa23a0d01d3bc10329801ffccbb7b313d1c5fc;hb=4803b343f52b716c80eed945fa12d7075399df1b;hp=4d68dadf9f682e89743593f00bcc0a2322494247;hpb=be73a507f4f3c1b40a77dd7fc587adaf45b4d8ea;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 4d68dadf9..45fa23a0d 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -34,7 +34,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = true
+let debug_printing = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -212,7 +212,10 @@ and pp_layout = function
   | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2)
   | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2)
   | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2)
-  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) (pp_term t2) (pp_term t3)
+  | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1)
+  (pp_term t2) (pp_term t3)
+  | Ast.Maction l -> sprintf "\\MACTION (%s)" 
+     (String.concat "," (List.map pp_term l))
   | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Ast.Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)