- (match List.nth context (n - 1 - k) with
- | (_,NCic.Decl _) -> config
- | (_,NCic.Def (x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s))
+ let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
+ (match x with
+ | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
+ | _ -> config)