From aa8e74a3f9b16a2fc2521b58a2413534bfb2641e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Nov 2007 21:46:15 +0000 Subject: [PATCH] Trivial bug fixed in type inference of LetIn source types. --- helm/software/components/cic_exportation/cicExportation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -> -- 2.39.2