- | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
- if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
- !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,(Cic.AMutConstruct _ as he::tl as args)) as t ->
+ (match LibraryObjects.destroy_nat t with
+ | Some n -> idref aid (Ast.Num (string_of_int n, -1))
+ | None ->
+ let deannot_he = Deannotate.deannotate_term he in
+ let coercion_info = CoercDb.is_a_coercion deannot_he in
+ if coercion_info <> None && !Acic2content.hide_coercions then
+ match coercion_info with
+ | None -> assert false
+ | Some (_,_,_,sats,cpos) ->
+ if cpos < List.length tl then
+ let _,rest =
+ try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[]
+ in
+ if rest = [] then
+ idref aid (List.nth (List.map k tl) cpos)
+ else
+ idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest)))
+ else
+ idref aid (Ast.Appl (List.map k tl))
+ else
+ idref aid (Ast.Appl (List.map k args)))