- transcript: bugfix

[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 51b66cacc8756f9b773f52bb95ec1edb621471a6..2e34b3c24555d4a2f5282209ac8aa35faf51e7f7 100644 (file)
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -15,9 +15,8 @@
 include "Z/compare.ma".
 include "Z/plus.ma".
 include "nat/factorization.ma".
+include "Q/fraction/fraction.ma".
 
-alias id "pp" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/1)".
-alias id "cons" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/3)".
 let rec enumerator_integral_fraction l ≝
  match l with
   [ pp n ⇒ Some ? l