]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/termAcicContent.ml
Huge commit:
[helm.git] / helm / software / components / acic_content / termAcicContent.ml
index cda76ce0914e44ccaae48e2f716fba326a9b8346..622a816181ba0489fa4ee4fcdba26e63572073cd 100644 (file)
@@ -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