Even more Q stuff moved around.

[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..960756abe8ba41573efc4b0c3ca8de782e3af516 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