From: Claudio Sacerdoti Coen Date: Thu, 8 Nov 2007 21:46:15 +0000 (+0000) Subject: Trivial bug fixed in type inference of LetIn source types. X-Git-Tag: 0.4.95@7852~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3c9a0cb82f346f7c3ba2347b6a61f5a7a78180d0 Trivial bug fixed in type inference of LetIn source types. --- 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) ->