X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;h=813e65c298bf9c5c9281597088dadf655b7db3e6;hb=3c9a0cb82f346f7c3ba2347b6a61f5a7a78180d0;hp=e671effca9a565645d8d7f8c41f780d8b13f5d38;hpb=d80bd0bc5253538759bfb13c98e86d07592a9359;p=helm.git

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index e671effca..813e65c29 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -182,7 +182,7 @@ let rec pp ~in_type t context =
             "(function " ^ ppname b ^ " -> " ^
              pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
     | C.LetIn (b,s,t) ->
-       let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
+       let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
        "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
         pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
     | C.Appl (C.MutInd _ as he::tl) ->