- cic_exportation, cic_acic, acic_content (only parts related to acic)

[helm.git] / matita / components / ng_cic_content / nTermCicContent.ml

diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml
index 5cfda009c26bb564af3a45205860d931c320befb..26d7e98fb553840521ff87efa667afd424924f4b 100644 (file)
--- a/matita/components/ng_cic_content/nTermCicContent.ml
+++ b/matita/components/ng_cic_content/nTermCicContent.ml
@@ -34,6 +34,8 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 type id = string
 
+let hide_coercions = ref true;;
+
 (*
 type interpretation_id = int
 
@@ -143,7 +145,7 @@ let nast_of_cic0 status
          | Some n -> idref (Ast.Num (string_of_int n, -1))
          | None ->
             let args =
-             if not !Acic2content.hide_coercions then args
+             if not !hide_coercions then args
              else
               match
                NCicCoercion.match_coercion status ~metasenv ~context ~subst t