+ (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+ && !hide_coercions ->
+ let cpos,sats =
+ match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> assert false
+ | Some (_,_,_,sats,cpos) -> cpos, sats
+ in
+ let x = List.nth tl cpos in
+ let _,rest =
+ try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[]