]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPp.ml
* various bug fix related to the environment returned when a match
[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml
index cb67202a5a6e73554303e44ace1bec4645cbe68a..696580cdc5442c97555cb9bea3cf64e5b0eb131b 100644 (file)
@@ -156,6 +156,8 @@ 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)
 
 and pp_fold_kind = function
   | `Left -> "left"