From 9e30dacbcdb10a58d6cf8f3995d1a195f2b31f4b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 21:20:22 +0000
Subject: [PATCH] Bug fixed: refinement of mutual recursive definitions used to
 invert the definitions.

---
 helm/software/components/ng_refiner/nCicRefiner.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index c52ab7e62..7cc2f33d2 100644
--- 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
 ;; 
 
-- 
2.39.2