let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
aux (k',e',t',s'@s)
| k, _, NCic.Rel n, s as config (* when n > k *) ->
- (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)
| (k, e, NCic.Meta (n,l), s) as config ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in