- (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 l t (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
- )
+ (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)