X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAstPp.ml;h=2479fe24a3bf4fab3d5b31cd74f3bddadfb4be89;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=bb365d73ccf70f14bf38e5c4e166d2bdcfd9396d;hpb=66a331a32509281f0c28ced014640e98a49cc0e0;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index bb365d73c..2479fe24a 100644
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -35,7 +35,6 @@ let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s
 
 let rec pp_term = function
   | CicAst.AttributedTerm (_, term) -> pp_term term
-
   | CicAst.Appl terms ->
       sprintf "(%s)" (String.concat " " (List.map pp_term terms))
   | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
@@ -50,6 +49,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)
+  | CicAst.Cast (t1,t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2)
   | CicAst.LetIn (var, t1, t2) ->
       sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1)
         (pp_term t2)
@@ -79,8 +79,7 @@ let rec pp_term = function
   | CicAst.Sort `Type -> "Type"
   | CicAst.Sort `CProp -> "CProp"
   | CicAst.Symbol (name, _) -> name
-
-  | CicAst.UserInput -> ""
+  | CicAst.UserInput -> "%"
 
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)