Trivial bug fixed in type inference of LetIn source types.

[helm.git] / components / cic_exportation / cicExportation.ml

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index c975ff11e8fb35ff92b192e698611f300af86431..813e65c298bf9c5c9281597088dadf655b7db3e6 100644 (file)
--- 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) ->
@@ -294,6 +294,10 @@ let rec pp ~in_type t context =
                      let rec aux argsno context =
                       function
                          Cic.Lambda (name,ty,bo) when argsno > 0 ->
+                          let name =
+                           match name with
+                              Cic.Anonymous -> Cic.Anonymous
+                            | Cic.Name n -> Cic.Name (ppid n) in
                           let args,res =
                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
                             bo