X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FtermAcicContent.ml;h=7948f2654ac51aa29cc79d13f12bbb3dd6a71534;hb=b65592962c5614981b20154000779805c3620075;hp=fddd777f7e13959fac65a76ff202f40ae23f4738;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index fddd777f7..7948f2654 100644
--- a/components/acic_content/termAcicContent.ml
+++ b/components/acic_content/termAcicContent.ml
@@ -66,6 +66,7 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
+
 let ast_of_acic0 term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
@@ -117,7 +118,23 @@ let ast_of_acic0 term_info acic k =
     | Cic.ALetIn (id,n,s,t) ->
         idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
           k s, k t))
-    | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
+    | 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))
     | Cic.AConst (id,uri,substs) ->
         register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))