X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=7948f2654ac51aa29cc79d13f12bbb3dd6a71534;hb=bdf989481462c1185c9cbbfdd4b31d13aa4352b3;hp=a25730e4d1fa0aed8e2279694d2d60d3a7d7deb7;hpb=7815a9150b5581f60e49ad6520f46ac287e073fa;p=helm.git

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index a25730e4d..7948f2654 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -66,7 +66,6 @@ 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 hide_coercions = ref true;;
 
 let ast_of_acic0 term_info acic k =
   let k = k term_info in
@@ -123,7 +122,7 @@ let ast_of_acic0 term_info acic k =
     | 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) &&
-          !hide_coercions
+          !Acic2content.hide_coercions
        then
         let rec last =
          function