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=c3185d6a251ba1ee2b63a1d8a4e63d80ebdfb453;hb=26cce624c98e795521078794c748758798031704;hp=696580cdc5442c97555cb9bea3cf64e5b0eb131b;hpb=f508a0d1a9202186ec9b913ce1ddc6861918ad64;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 696580cdc..c3185d6a2 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -158,6 +158,8 @@ and pp_magic = function
       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)
 
 and pp_fold_kind = function
   | `Left -> "left"