X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FtermAcicContent.ml;h=622a816181ba0489fa4ee4fcdba26e63572073cd;hb=7008966fdd5b3811852f60b459572a347be932a0;hp=cda76ce0914e44ccaae48e2f716fba326a9b8346;hpb=213cc7cf3c9da7c024b44b54e07035b831f7a31f;p=helm.git

diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index cda76ce09..622a81618 100644
--- a/components/acic_content/termAcicContent.ml
+++ b/components/acic_content/termAcicContent.ml
@@ -141,9 +141,9 @@ let ast_of_acic0 term_info acic k =
            | 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
+       if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
        then
-         match CoercGraph.is_a_coercion_to_funclass deannot_he with
+         match CoercDb.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