(match List.nth context (n-1) with
Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
| Some (_, C.Def bo) -> whdaux l (S.lift n bo)
- | None -> raise RelToHiddenHypothesis
+ | None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) as t ->
(match CicEnvironment.get_cooked_obj ~trust:false uri with