;;
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
;;
| 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), _ =