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=f98b5106719c4e5eda957dd98968c4a44ee2976b;hb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;hp=fcb42fd1853a869264b9599faf80aa45d98d240e;hpb=b24260fd5c00791ad04042405e3942f288f54ab2;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index fcb42fd18..f98b51067 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -62,6 +62,7 @@ let rec pp_term = function
       sprintf "%smatch %s with %s"
         (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t))
         (pp_term term) (pp_patterns patterns)
+  | Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
   | LetIn (var, t1, t2) ->
       sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
         (pp_term t2)