- (try
- match List.nth context (n-1) with
- Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def (bo,_)) ->
- try_delta_expansion context l t (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
- with
- Failure _ -> assert false)