some work on Q

[helm.git] / helm / software / matita / contribs / dama / dama / depends

diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends
index dcbfcc6f0adcabc26fcf4a7f0a6d60d92e2f0ef5..3299c9a2f1d5046bed0fc6fea0155ffa98b549c1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/depends
+++ b/helm/software/matita/contribs/dama/dama/depends
@@ -1,38 +1,29 @@
-metric_lattice.ma excess.ma lattice.ma metric_space.ma
-metric_space.ma ordered_divisible_group.ma
-sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma tend.ma
-premetric_lattice.ma lattice.ma metric_space.ma
-ordered_group.ma group.ma
-divisible_group.ma group.ma nat/orders.ma
-ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
-sequence.ma excess.ma
-constructive_connectives.ma logic/connectives.ma
-group.ma excess.ma
-prevalued_lattice.ma ordered_group.ma
-excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
-sandwich_corollary.ma sandwich.ma
-Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
-limit.ma excess.ma infsup.ma metric_lattice.ma tend.ma
-lattice.ma excess.ma
-tend.ma metric_space.ma nat/orders.ma sequence.ma
-constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
-infsup.ma excess.ma sequence.ma
-constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma
-classical_pointwise/topology.ma classical_pointwise/sets.ma
-classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma
-classical_pointwise/sets.ma logic/connectives.ma nat/nat.ma
-classical_pointfree/ordered_sets.ma excess.ma
-classical_pointfree/ordered_sets2.ma classical_pointfree/ordered_sets.ma
-attic/fields.ma attic/rings.ma
-attic/reals.ma attic/ordered_fields_ch0.ma
-attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma
-attic/vector_spaces.ma attic/reals.ma
-attic/rings.ma group.ma
-attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma
-Q/q.ma 
-higher_order_defs/relations.ma 
-logic/connectives.ma 
+sandwich.ma ordered_uniform.ma
+property_sigma.ma ordered_uniform.ma russell_support.ma
+uniform.ma supremum.ma
+bishop_set.ma ordered_set.ma
+sequence.ma nat/nat.ma
+ordered_uniform.ma uniform.ma
+supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma
+property_exhaustivity.ma ordered_uniform.ma property_sigma.ma
+bishop_set_rewrite.ma bishop_set.ma
+cprop_connectives.ma logic/equality.ma
+nat_ordered_set.ma bishop_set.ma nat/compare.ma
+lebesgue.ma property_exhaustivity.ma sandwich.ma
+ordered_set.ma cprop_connectives.ma
+russell_support.ma cprop_connectives.ma nat/nat.ma
+models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
+models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
+models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
+models/q_function.ma Q/q/q.ma cprop_connectives.ma list/list.ma
+models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma
+models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
+models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma
+Q/q/q.ma 
+datatypes/constructors.ma 
+list/list.ma 
+logic/equality.ma 
+nat/compare.ma 
+nat/le_arith.ma 
 nat/nat.ma 
-nat/orders.ma 
 nat/plus.ma 
-nat/times.ma