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: make_still_working~5882 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa8e74a3f9b16a2fc2521b58a2413534bfb2641e;p=helm.git Trivial bug fixed in type inference of LetIn source types. --- diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index e671effca..813e65c29 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/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) ->