From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 May 2009 21:20:22 +0000 (+0000)
Subject: Bug fixed: refinement of mutual recursive definitions used to invert the
X-Git-Tag: make_still_working~4004
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e30dacbcdb10a58d6cf8f3995d1a195f2b31f4b;p=helm.git

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 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
 ;;