From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Feb 2007 18:46:35 +0000 (+0000)
Subject: Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
X-Git-Tag: 0.4.95@7852~628
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7bfd6bb04dd067edcd2074587d571e57be5b84b;p=helm.git

Incredible bug fixed in Fix and CoFix. The types of the mutual inductive
functions were not lifted when added to the context.
---

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 8f36b9e17..5dc425489 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/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) ->