Fixed a bug in the undebruijnate function which caused the refiner to produce

a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7833b9c4a202e55f8380f401f4c4e408cb15f156..ec4747781a646371d729e12098ad523f096d1c8e 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -993,13 +993,15 @@ let relocalise old_localise dt t add =
 ;;
 
 let undebruijnate inductive ref t rev_fl =
+  let len = List.length rev_fl in 
   NCicSubstitution.psubst (fun x -> x) 
-   (List.rev (HExtlib.list_mapi 
+   (HExtlib.list_mapi 
       (fun (_,_,rno,_,_,_) i -> 
+         let i = len - i - 1 in
          NCic.Const 
            (if inductive then NReference.mk_fix i rno ref
             else NReference.mk_cofix i ref))
-      rev_fl))
+      rev_fl)
     t
 ;;