- 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 960756abe8ba41573efc4b0c3ca8de782e3af516..f16851f016bfcc983478224574171e2f792fc0a5 100644 (file)
--- 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 ≝