snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index c3185d6a251ba1ee2b63a1d8a4e63d80ebdfb453..f8b8acba03be7ecbdccc01b94cf8d2dc29cc71df 100644 (file)
--- 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"