Huge commit:

[helm.git] / helm / software / components / acic_content / acic2content.ml

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index 23d6447863a9f9335f101d240e1edfa51ca885dd..a2e7622ea6549d6ee1b87941e95daa150b126c36 100644 (file)
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -805,7 +805,7 @@ and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
     | ((Cic.AConst _) as he)::tl
     | ((Cic.AMutInd _) as he)::tl
     | ((Cic.AMutConstruct _) as he)::tl when 
-       CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
        !hide_coercions ->
         let rec last =
          function