]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/depends
Even more Q stuff moved around.
[helm.git] / helm / software / matita / library / depends
index b17029e9226db6deb50c1fc949d3a11dc55bceb6..2ae7107a4c6180b98c74dc463fc8cce3363ec47e 100644 (file)
@@ -32,7 +32,8 @@ 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