X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq%2Fq.ma;h=f16851f016bfcc983478224574171e2f792fc0a5;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=960756abe8ba41573efc4b0c3ca8de782e3af516;hpb=e85acd6f01bccc0b4a6750dd6d2710d7b511948a;p=helm.git

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 960756abe..f16851f01 100644
--- a/helm/software/matita/library/Q/q/q.ma
+++ b/helm/software/matita/library/Q/q/q.ma
@@ -21,6 +21,8 @@ inductive Q : Set \def
   | Qpos : ratio  \to Q
   | Qneg : ratio  \to Q.
 
+interpretation "Rationals" 'Q = Q.
+
 definition Qone ≝ Qpos one.
 
 definition Qopp ≝