X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=50312ff12e117d7208fcbc6437400305bd317c52;hb=3b2361afb73203749541ad07e94648da6057ae67;hp=236b985075b022605a7e95b297fe5e844c414ea1;hpb=413007de240fefb28650bb5ba7940f46db656751;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 236b98507..50312ff12 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -116,9 +116,9 @@ let rec pp_term ?(pp_parens = true) 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,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)
+(*       let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
+        sprintf "let %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) ->