- transcript: bugfix

[helm.git] / helm / software / matita / library / Q / q / q.ma

diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma
index 43b090fef3f3f30139460c85521e46d8d032d72f..f16851f016bfcc983478224574171e2f792fc0a5 100644 (file)
--- 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 ≝