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