X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FtermAcicContent.ml;h=516d5f5429ab56926e92e426ca654a45511b2ee5;hb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;hp=7948f2654ac51aa29cc79d13f12bbb3dd6a71534;hpb=f764844fa35ab0bb9c10707151340b924060f069;p=helm.git

diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index 7948f2654..516d5f542 100644
--- a/components/acic_content/termAcicContent.ml
+++ b/components/acic_content/termAcicContent.ml
@@ -121,16 +121,31 @@ let ast_of_acic0 term_info acic k =
     | 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
+       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
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
-        in
-         idref aid (k (last tl))
+         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,args) ->