From a2079b129bcb754d55a5ed5290d8b9aaa525ac3e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Feb 2007 18:46:35 +0000 Subject: [PATCH] Incredible bug fixed in Fix and CoFix. The types of the mutual inductive functions were not lifted when added to the context. --- .../cic_proof_checking/cicTypeChecker.ml | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 8f36b9e17..5dc425489 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1834,16 +1834,15 @@ end; in outtype,ugraph5 | C.Fix (i,fl) -> - let types_times_kl,ugraph1 = + let types,kl,ugraph1,len = (* WAS: list rev list map *) List.fold_left - (fun (l,ugraph) (n,k,ty,_) -> + (fun (types,kl,ugraph,len) (n,k,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + k::kl,ugraph1,len+1) + ) ([],[],ugraph,0) fl in - let (types,kl) = List.split types_times_kl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (name,x,ty,bo) -> @@ -1877,15 +1876,15 @@ end; let (_,_,ty,_) = List.nth fl i in ty,ugraph2 | C.CoFix (i,fl) -> - let types,ugraph1 = + let types,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,ty,_) -> + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl ty))::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + ugraph1,len+1) + ) ([],ugraph,0) fl in - let len = List.length types in let ugraph2 = List.fold_left (fun ugraph (_,ty,bo) -> -- 2.39.2