+ | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
+ | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
+ | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
+ if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+ !Acic2content.hide_coercions
+ then
+ let rec last =
+ function
+ [] -> assert false
+ | [t] -> t
+ | _::tl -> last tl
+ in
+ idref aid (k (last tl))
+ else
+ idref aid (Ast.Appl (List.map k args))
+ | Cic.AAppl (aid,args) ->
+ idref aid (Ast.Appl (List.map k args))