X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=5a85a1289297301031355cf3bf3dfa4cae83f921;hb=117dfe4f3b6d8ebf53172eaf66b628a27e4e43e1;hp=7833b9c4a202e55f8380f401f4c4e408cb15f156;hpb=e7e2954471b4779cd4e4ae590ca5047575902fb7;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7833b9c4a..5a85a1289 100644
--- 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
 ;; 
 
@@ -1133,7 +1135,7 @@ let typeof_obj
                   | NCic.Meta _ -> metasenv, subst
                   | NCic.Implicit _ -> metasenv, subst
                   | NCic.Appl (NCic.Rel i :: args) as t
-                      when i >= List.length context - len ->
+                      when i > List.length context - len ->
                       let lefts, _ = HExtlib.split_nth leftno args in
                       let ctxlen = List.length context in
                       let (metasenv, subst), _ =