X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=e04b00b7057cbd622fce15ed55daee247e07057b;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=cb67202a5a6e73554303e44ace1bec4645cbe68a;hpb=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index cb67202a5..e04b00b70 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -36,12 +36,10 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal l =
-  sprintf "literal(%s)"
-    (match l with
-    | `Symbol s
-    | `Keyword s
-    | `Number s -> s)
+let pp_literal = function
+  | `Symbol s -> sprintf "symbol(%s)" s
+  | `Keyword s -> sprintf "keyword(%s)" s
+  | `Number s -> sprintf "number(%s)" s
 
 let rec pp_term = function
   | AttributedTerm (`Href _, term) when print_attributes ->
@@ -138,7 +136,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,6 +154,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_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"