Bug fixed: refinement of mutual recursive definitions used to invert the

definitions.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index c52ab7e62a90002776f77b312e4d6e91d5ffd179..7cc2f33d277d1198fee450e70d74277994b776e3 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -524,12 +524,12 @@ let relocalise old_localise dt t add =
 
 let undebruijnate inductive ref t rev_fl =
   NCicSubstitution.psubst (fun x -> x) 
-    (HExtlib.list_mapi 
+   (List.rev (HExtlib.list_mapi 
       (fun (_,_,rno,_,_,_) i -> 
          NCic.Const 
            (if inductive then NReference.mk_fix i rno ref
             else NReference.mk_cofix i ref))
-      rev_fl)
+      rev_fl))
     t
 ;;