X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=622a816181ba0489fa4ee4fcdba26e63572073cd;hb=3f676ab6acafa32514a44bc84d287f44dbc5389e;hp=cda76ce0914e44ccaae48e2f716fba326a9b8346;hpb=774c8d18f41e71ae7e26a90d726d10a6f95de1fe;p=helm.git

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index cda76ce09..622a81618 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/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