Several instances of the same bug fixed at once: when processing a Fix,

[helm.git] / helm / software / components / tactics / proofEngineReduction.ml

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 1b5922d1d28f8f0af33c462f55ea1d07d21faa18..f72ec4679842b9888bed5b07b9e92bc48fd50b28 100644 (file)
--- 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' =