Even more Q stuff moved around.

[helm.git] / helm / software / matita / library / depends

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index bbf2c8079d94c7b883defd8e08ac2413c3a28cb9..2ae7107a4c6180b98c74dc463fc8cce3363ec47e 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -21,9 +21,8 @@ higher_order_defs/ordering.ma logic/equality.ma
 higher_order_defs/relations.ma logic/connectives.ma
 Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-Q/frac.ma Q/q.ma nat/factorization.ma
+Q/frac.ma 
 Q/inv.ma Q/q.ma
-Q/Qplus_andrea.ma Q/frac.ma nat/factorization.ma
 Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
 Q/q/q.ma Q/ratio/ratio.ma
 Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
@@ -33,7 +32,9 @@ Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma
 Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma
 Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma
 Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma
-Q/fraction/ftimes.ma Q/fraction/finv.ma Q/ratio/ratio.ma
+Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma
+Q/fraction/numerator_denominator.ma Q/fraction/finv.ma
+Q/nat_fact/times.ma nat/factorization.ma
 datatypes/compare.ma 
 datatypes/constructors.ma logic/equality.ma
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma