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: make_still_working~6487
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2079b129bcb754d55a5ed5290d8b9aaa525ac3e;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/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) ->