made matita.runtime_base_dir overridable setting MATITA_RUNTIME_BASE_DIR env variable

[helm.git] / components / cic_proof_checking / cicReduction.ml

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index 576721be3542c1b67a098c05f0fbbadede1e2f85..213aa2356bd1e3d9940efccdc4420f1e7dd05b2b 100644 (file)
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -712,12 +712,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                     let leng = List.length fl in
                     let new_env =
                      let counter = ref 0 in
-                     let rec build_env e =
-                      if !counter = leng then e
+                     let rec build_env e' =
+                      if !counter = leng then e'
                       else
                        (incr counter ;
                         build_env
-                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e))
+                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
                      in
                       build_env e
                     in
@@ -973,8 +973,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys =
-              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,_,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
             in
             if i1 = i2 then
              List.fold_right2
@@ -992,9 +996,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
+            in
             if i1 = i2 then
               List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->