- | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
- let last_n n l =
- let rec aux =
- function
- [] -> assert false
- | [_] as l -> l,1
- | he::tl ->
- let (res,len) as res' = aux tl in
- if len < n then
- he::res,len + 1
- else
- res'
- in
- match fst (aux l) with
- [] -> assert false
- | [t] -> t
- | Ast.AttributedTerm (_,(Ast.Appl l))::tl ->
- idref aid (Ast.Appl (l@tl))
- | l -> idref aid (Ast.Appl l)
- in
- let deannot_he = Deannotate.deannotate_term he in
- if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
- then
- match CoercGraph.is_a_coercion_to_funclass deannot_he with
- | None -> idref aid (last_n 1 (List.map k tl))
- | Some i -> idref aid (last_n (i+1) (List.map k 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)))