X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineReduction.ml;h=f72ec4679842b9888bed5b07b9e92bc48fd50b28;hb=9b57abaabd8f66607062c3f33e74928f61468060;hp=1b5922d1d28f8f0af33c462f55ea1d07d21faa18;hpb=38d3574438b4f764ad433915c9733cc73a684b39;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 1b5922d1d..f72ec4679 100644
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -587,8 +587,12 @@ let reduce context =
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let tys =
-        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        in
         let t' () =
          let fl' =
@@ -625,8 +629,12 @@ let reduce context =
              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
            )
     | C.CoFix (i,fl) ->
-       let tys =
-        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        in
         let t' =
          let fl' =
@@ -819,8 +827,12 @@ let simpl context =
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let tys =
-        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+         List.fold_left
+           (fun (types,len) (n,_,ty,_) ->
+              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+               len+1)
+	   ) ([],0) fl
        in
         let t' () =
          let fl' =
@@ -857,8 +869,12 @@ let simpl context =
              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
            )
     | C.CoFix (i,fl) ->
-       let tys =
-        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        in
         let t' =
          let fl' =