fix with m (to be optimized) are rewritten such that m is abtracted outside the fix

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

diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index a10d64a303fefd0a782064403488b3ad110dbc27..f89dbc33543a02e46abff4d7f27d3ec5cb7785ce 100644 (file)
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -73,10 +73,6 @@ nat/o.ma nat/binomial.ma nat/sqrt.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
 Q/q.ma Z/compare.ma Z/plus.ma
 technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
-Fsub/part1a.ma Fsub/defn.ma
-Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma
-Fsub/defn.ma Fsub/util.ma
-Fsub/part1a_inversion.ma Fsub/defn.ma
 decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
 decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
 decidable_kit/fgraph.ma decidable_kit/fintype.ma