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

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

diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli
index 2a1d7bcc7c613dd1c07c7652d5cf15eef438a0d5..38c0ebf3cebdcd35b7223323da694c528ca44ead 100644 (file)
--- a/matita/components/ng_cic_content/nTermCicContent.mli
+++ b/matita/components/ng_cic_content/nTermCicContent.mli
@@ -85,6 +85,8 @@ val nast_of_cic :
 
 type id = string
 
+val hide_coercions: bool ref
+
 val nmap_sequent:
  #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   int * NCic.conjecture ->