X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=2e34b3c24555d4a2f5282209ac8aa35faf51e7f7;hb=f524a0d716de2bdc0874aace8f82f6289034eccf;hp=683ddeb8822fa04a0474d91282c951fccbe8c1ce;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 683ddeb88..2e34b3c24 100644
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -15,6 +15,7 @@
 include "Z/compare.ma".
 include "Z/plus.ma".
 include "nat/factorization.ma".
+include "Q/fraction/fraction.ma".
 
 let rec enumerator_integral_fraction l ≝
  match l with
@@ -57,6 +58,7 @@ let rec denominator_integral_fraction l ≝
        ]
   ].
 
+(*
 definition enumerator_of_fraction ≝
  λq.
   match q with
@@ -94,3 +96,4 @@ definition denominator ≝
    | Qpos r ⇒ denominator_of_fraction r
    | Qneg r ⇒ denominator_of_fraction r
    ].
+*)
\ No newline at end of file