X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=ae33d1f83ce4a3d31f391a1ebef36844857c8c07;hb=25be562c5436746df8d892449a9ff98755c37e9f;hp=477e775d8dfe8cca961a6e892c042398db91a059;hpb=18d61b8fe9cda8874a3f57b70a293492460ae574;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 477e775d8..ae33d1f83 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -241,9 +241,9 @@ let cic2grafite context menv t =
       | Cic.Prod (Cic.Name n, s, t) ->
           PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
-      | Cic.LetIn (Cic.Name n, s, t) ->
+      | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
-            aux (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+            aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
       | Cic.Meta _ -> PT.Implicit
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set