Many changes

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

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 683ddeb8822fa04a0474d91282c951fccbe8c1ce..2e34b3c24555d4a2f5282209ac8aa35faf51e7f7 100644 (file)
--- 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