X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=f8b8acba03be7ecbdccc01b94cf8d2dc29cc71df;hb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;hp=c3185d6a251ba1ee2b63a1d8a4e63d80ebdfb453;hpb=fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index c3185d6a2..f8b8acba0 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -138,7 +138,7 @@ and pp_layout = function
   | Sqrt t -> sprintf "\\SQRT %s" (pp_term t)
   | Root (arg, index) ->
       sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg)
-(*   | Break -> "\\BREAK" *)
+  | Break -> "\\BREAK"
 (*   | Space -> "\\SPACE" *)
   | Box (box_spec, terms) ->
       sprintf "\\%s [%s]" (pp_box_spec box_spec)
@@ -156,10 +156,10 @@ and pp_magic = function
         (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec)
   | Default (p_some, p_none) ->
       sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none)
-  | If (p_guard, p) ->
-      sprintf "\\IF \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p)
-  | Unless (p_guard, p) ->
-      sprintf "\\UNLESS \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p)
+  | If (p_test, p_true, p_false) ->
+      sprintf "\\IF \\[%s\\] \\[%s\\] \\[%s\\]"
+	(pp_term p_test) (pp_term p_true) (pp_term p_false)
+  | Fail -> "\\FAIL"
 
 and pp_fold_kind = function
   | `Left -> "left"