X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=236b985075b022605a7e95b297fe5e844c414ea1;hb=da26f5476270e7d00f9a03b28b4db886c4557b6d;hp=4bd2f93ed2c633a8e0bb902d83e9bf50189301d6;hpb=87bdd061d096c836a02c77aa26e80d9c36180fad;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 4bd2f93ed..236b98507 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -115,9 +115,12 @@ let rec pp_term ?(pp_parens = true) t =
 	  (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
-    | Ast.LetIn (var, t1, t2) ->
-        sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
+    | Ast.LetIn ((var,t2), t1, t3) ->
+       let t2 = match t2 with None -> Ast.Implicit | Some t -> t in
+        sprintf "let %s : %s \\def %s in %s" (pp_term var)
           (pp_term ~pp_parens:true t2)
+          (pp_term ~pp_parens:true t1)
+          (pp_term ~pp_parens:true t3)
     | Ast.LetRec (kind, definitions, term) ->
 	let rec get_guard i = function
 	   | []                   -> (*assert false*) Ast.Implicit