merged cic_notation with disambiguation: good luck!

[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 fcb42fd1853a869264b9599faf80aa45d98d240e..f98b5106719c4e5eda957dd98968c4a44ee2976b 100644 (file)
--- 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)