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

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 43b090fef..f16851f01 100644
--- a/helm/software/matita/library/Q/q/q.ma
+++ b/helm/software/matita/library/Q/q/q.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "Q/ratio/ratio.ma".
+include "Q/fraction/numerator_denominator.ma".
 
 (* a rational number is either O or a ratio with a sign *)
 inductive Q : Set \def 
@@ -20,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 ≝