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