metavariable context has a separator now

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_support.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma
index 6694a033fa6494902a7f499a95eff54063faf569..70b3e6ade4b21544c6385be1d58b313167f50ec8 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -14,10 +14,9 @@
 
 include "Q/q/qtimes.ma".
 include "Q/q/qplus.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
-notation "\rationals" non associative with precedence 99 for @{'q}.
-interpretation "Q" 'q = Q. 
+interpretation "Q" 'Q = Q. 
 
 (* group over Q *)
 axiom qp : ℚ → ℚ → ℚ.