cicUtil: we moved here pp_term from proceduralHelpers

[helm.git] / helm / software / matita / contribs / procedural / Coq / depends

diff --git a/helm/software/matita/contribs/procedural/Coq/depends b/helm/software/matita/contribs/procedural/Coq/depends
index 5088e5f29fc6d365834353b7dd23a3739b395a93..93dcd84fec668b31f5cfb9bb65db225033941bba 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/depends
+++ b/helm/software/matita/contribs/procedural/Coq/depends
@@ -22,7 +22,7 @@ ZArith/Zsqrt.ma ZArith/Zsqrt.mma
 Reals/Rseries.mma Arith/Compare.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma
 Lists/ListSet.mma Coq.ma Lists/List.ma
 Arith/Le.ma Arith/Le.mma
-Setoids/Setoid.mma Coq.ma
+Setoids/Setoid.mma Coq.ma Init/Prelude.ma
 Logic/ProofIrrelevance.ma Logic/ProofIrrelevance.mma
 ZArith/Zeven.mma Coq.ma ZArith/BinInt.ma
 ZArith/Zcompare.mma Arith/Gt.ma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma
@@ -35,11 +35,11 @@ Reals/Ranalysis4.mma Coq.ma Reals/Exp_prop.ma Reals/Ranalysis1.ma Reals/Ranalysi
 Coq.ma preamble.ma
 ZArith/Znat.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
 Reals/Integration.ma Reals/Integration.mma
-Logic/RelationalChoice.mma Coq.ma
+Logic/RelationalChoice.mma Coq.ma Init/Prelude.ma
 ZArith/Zpower.ma ZArith/Zpower.mma
 Init/Prelude.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma Init/Peano.ma Init/Specif.ma Init/Wf.ma
 Bool/IfProp.mma Bool/Bool.ma Coq.ma
-Arith/Even.mma Coq.ma
+Arith/Even.mma Coq.ma Init/Prelude.ma
 Lists/TheoryList.ma Lists/TheoryList.mma
 Arith/Wf_nat.ma Arith/Wf_nat.mma
 IntMap/Mapsubset.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapiter.ma ZArith/ZArith.ma
@@ -48,7 +48,7 @@ Wellfounded/Wellfounded.ma Wellfounded/Wellfounded.mma
 Sets/Multiset.ma Sets/Multiset.mma
 Logic/ClassicalFacts.ma Logic/ClassicalFacts.mma
 Reals/RiemannInt.mma Arith/Max.ma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/RiemannInt_SF.ma Reals/SeqSeries.ma
-Wellfounded/Inverse_Image.mma Coq.ma
+Wellfounded/Inverse_Image.mma Coq.ma Init/Prelude.ma
 Reals/Rsigma.ma Reals/Rsigma.mma
 Bool/BoolEq.ma Bool/BoolEq.mma
 Wellfounded/Disjoint_Union.ma Wellfounded/Disjoint_Union.mma
@@ -72,7 +72,7 @@ Wellfounded/Union.ma Wellfounded/Union.mma
 Sets/Uniset.ma Sets/Uniset.mma
 Sorting/Sorting.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma
 Init/Wf.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
-Sets/Ensembles.mma Coq.ma
+Sets/Ensembles.mma Coq.ma Init/Prelude.ma
 Reals/Cos_plus.mma Arith/Max.ma Coq.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
 Reals/SplitAbsolu.mma Coq.ma Reals/Rbasic_fun.ma
 Relations/Operators_Properties.ma Relations/Operators_Properties.mma
@@ -83,10 +83,10 @@ Logic/Decidable.ma Logic/Decidable.mma
 Arith/Div.ma Arith/Div.mma
 Sets/Relations_3_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma Sets/Relations_2_facts.ma Sets/Relations_3.ma
 Arith/Compare.ma Arith/Compare.mma
-Logic/Hurkens.mma Coq.ma
+Logic/Hurkens.mma Coq.ma Init/Prelude.ma
 Arith/Min.mma Arith/Arith.ma Coq.ma
 Reals/R_sqr.mma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma
-Bool/Bool.mma Coq.ma
+Bool/Bool.mma Coq.ma Init/Prelude.ma
 Reals/Alembert.ma Reals/Alembert.mma
 IntMap/Allmaps.mma Coq.ma IntMap/Adalloc.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapc.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapfold.ma IntMap/Mapiter.ma IntMap/Maplists.ma IntMap/Mapsubset.ma
 Sets/Relations_2.mma Coq.ma Sets/Relations_1.ma
@@ -142,7 +142,7 @@ Sets/Powerset_facts.mma Coq.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensemb
 Reals/Alembert.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
 ZArith/Zbool.ma ZArith/Zbool.mma
 Sets/Partial_Order.mma Coq.ma Sets/Ensembles.ma Sets/Relations_1.ma
-Logic/ClassicalFacts.mma Coq.ma
+Logic/ClassicalFacts.mma Coq.ma Init/Prelude.ma
 Reals/Rdefinitions.mma Coq.ma ZArith/ZArith_base.ma
 Reals/PSeries_reg.ma Reals/PSeries_reg.mma
 IntMap/Adalloc.ma IntMap/Adalloc.mma
@@ -172,7 +172,7 @@ Logic/Diaconescu.mma Bool/Bool.ma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalFac
 Reals/Rbase.mma Coq.ma Reals/DiscrR.ma Reals/RIneq.ma Reals/Raxioms.ma Reals/Rdefinitions.ma
 Sets/Powerset_facts.ma Sets/Powerset_facts.mma
 IntMap/Adist.mma Arith/Arith.ma Arith/Min.ma Bool/Bool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma
-NArith/BinPos.mma Coq.ma
+NArith/BinPos.mma Coq.ma Init/Prelude.ma
 Lists/Streams.ma Lists/Streams.mma
 NArith/NArith.ma NArith/NArith.mma
 Relations/Newman.ma Relations/Newman.mma
@@ -201,14 +201,14 @@ Reals/Reals.ma Reals/Reals.mma
 Arith/Mult.ma Arith/Mult.mma
 ZArith/Wf_Z.ma ZArith/Wf_Z.mma
 Arith/Div.mma Arith/Compare_dec.ma Arith/Le.ma Coq.ma
-Arith/EqNat.mma Coq.ma
-Bool/DecBool.mma Coq.ma
+Arith/EqNat.mma Coq.ma Init/Prelude.ma
+Bool/DecBool.mma Coq.ma Init/Prelude.ma
 Arith/Minus.ma Arith/Minus.mma
 ZArith/Zbool.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zorder.ma
 NArith/BinNat.mma Coq.ma NArith/BinPos.ma
 Logic/Classical_Type.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma
 Wellfounded/Transitive_Closure.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
-Logic/Eqdep.mma Coq.ma
+Logic/Eqdep.mma Coq.ma Init/Prelude.ma
 Reals/Rtrigo_reg.ma Reals/Rtrigo_reg.mma
 Init/Specif.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
 Sets/Infinite_sets.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
@@ -232,7 +232,7 @@ Reals/PSeries_reg.mma Arith/Even.ma Arith/Max.ma Coq.ma Reals/Ranalysis1.ma Real
 NArith/NArith.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma
 NArith/BinNat.ma NArith/BinNat.mma
 ZArith/ZArith_dec.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
-Relations/Relation_Definitions.mma Coq.ma
+Relations/Relation_Definitions.mma Coq.ma Init/Prelude.ma
 Sorting/Sorting.ma Sorting/Sorting.mma
 Sets/Image.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
 Reals/Rlimit.mma Coq.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma
@@ -241,7 +241,7 @@ Reals/NewtonInt.ma Reals/NewtonInt.mma
 Reals/Rtrigo_def.ma Reals/Rtrigo_def.mma
 IntMap/Adalloc.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma ZArith/ZArith.ma
 Reals/Rgeom.ma Reals/Rgeom.mma
-Bool/Sumbool.mma Coq.ma
+Bool/Sumbool.mma Coq.ma Init/Prelude.ma
 Arith/Compare_dec.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Decidable.ma
 Sorting/Permutation.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma
 Sets/Classical_sets.mma Coq.ma Logic/Classical_Type.ma Sets/Constructive_sets.ma Sets/Ensembles.ma
@@ -265,7 +265,7 @@ IntMap/Mapaxioms.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/
 IntMap/Mapiter.ma IntMap/Mapiter.mma
 Reals/SplitAbsolu.ma Reals/SplitAbsolu.mma
 Reals/Ranalysis3.ma Reals/Ranalysis3.mma
-Logic/ChoiceFacts.mma Coq.ma
+Logic/ChoiceFacts.mma Coq.ma Init/Prelude.ma
 Reals/Ranalysis3.mma Coq.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Rbase.ma Reals/Rfunctions.ma
 Arith/Lt.mma Arith/Le.ma Coq.ma
 Reals/Rpower.mma Coq.ma Reals/Exp_prop.ma Reals/MVT.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Ranalysis4.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
@@ -273,7 +273,7 @@ Reals/Rderiv.ma Reals/Rderiv.mma
 Reals/Cos_plus.ma Reals/Cos_plus.mma
 Reals/MVT.ma Reals/MVT.mma
 Reals/SeqProp.ma Reals/SeqProp.mma
-Arith/Le.mma Coq.ma
+Arith/Le.mma Coq.ma Init/Prelude.ma
 ZArith/auxiliary.ma ZArith/auxiliary.mma
 Sets/Powerset.mma Coq.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
 Reals/SeqSeries.mma Arith/Max.ma Coq.ma Reals/Alembert.ma Reals/AltSeries.ma Reals/Binomial.ma Reals/Cauchy_prod.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rprod.ma Reals/Rseries.ma Reals/Rsigma.ma Reals/SeqProp.ma
@@ -281,14 +281,14 @@ Reals/RiemannInt.ma Reals/RiemannInt.mma
 IntMap/Mapfold.ma IntMap/Mapfold.mma
 Wellfounded/Lexicographic_Product.mma Coq.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
 Sets/Integers.ma Sets/Integers.mma
-Logic/Berardi.mma Coq.ma
+Logic/Berardi.mma Coq.ma Init/Prelude.ma
 IntMap/Mapcard.ma IntMap/Mapcard.mma
 ZArith/Zlogarithm.ma ZArith/Zlogarithm.mma
 ZArith/Zhints.mma Coq.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/Zabs.ma ZArith/Zcompare.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma
 Reals/Cauchy_prod.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
 Lists/MonoList.ma Lists/MonoList.mma
 Reals/Integration.mma Coq.ma Reals/NewtonInt.ma Reals/RiemannInt.ma Reals/RiemannInt_SF.ma
-Sets/Permut.mma Coq.ma
+Sets/Permut.mma Coq.ma Init/Prelude.ma
 Reals/Rtrigo_calc.ma Reals/Rtrigo_calc.mma
 Reals/DiscrR.ma Reals/DiscrR.mma
 Sets/Relations_2_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma
@@ -329,7 +329,7 @@ Reals/NewtonInt.mma Coq.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma
 NArith/Pnat.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma
 Sets/Relations_3_facts.ma Sets/Relations_3_facts.mma
 Reals/MVT.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtopology.ma
-Sets/Relations_1.mma Coq.ma
+Sets/Relations_1.mma Coq.ma Init/Prelude.ma
 IntMap/Fset.ma IntMap/Fset.mma
 Logic/JMeq.mma Coq.ma Logic/Eqdep.ma
 ZArith/Zsqrt.mma Coq.ma ZArith/ZArith_base.ma
@@ -364,10 +364,10 @@ Reals/Rtrigo.ma Reals/Rtrigo.mma
 Reals/ArithProp.mma Arith/Div2.ma Arith/Even.ma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma
 Reals/Ranalysis2.ma Reals/Ranalysis2.mma
 Arith/Wf_nat.mma Arith/Lt.ma Coq.ma
-Logic/Eqdep_dec.mma Coq.ma
+Logic/Eqdep_dec.mma Coq.ma Init/Prelude.ma
 Reals/Rcomplete.ma Reals/Rcomplete.mma
 Sets/Ensembles.ma Sets/Ensembles.mma
-Logic/Decidable.mma Coq.ma
+Logic/Decidable.mma Coq.ma Init/Prelude.ma
 ZArith/Zabs.ma ZArith/Zabs.mma
 ZArith/Zmin.ma ZArith/Zmin.mma
 Sets/Powerset_Classical_facts.mma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_facts.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
@@ -378,13 +378,13 @@ Sets/Finite_sets.mma Coq.ma Sets/Constructive_sets.ma Sets/Ensembles.ma
 ZArith/Zbinary.ma ZArith/Zbinary.mma
 Arith/Arith.ma Arith/Arith.mma
 Logic/ClassicalDescription.ma Logic/ClassicalDescription.mma
-Lists/Streams.mma Coq.ma
+Lists/Streams.mma Coq.ma Init/Prelude.ma
 Reals/SeqProp.mma Arith/Max.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
 Reals/RIneq.mma Coq.ma Reals/Raxioms.ma
 ZArith/ZArith.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma ZArith/Zlogarithm.ma ZArith/Zpower.ma ZArith/Zsqrt.ma
 Sorting/Heap.ma Sorting/Heap.mma
 Sets/Cpo.ma Sets/Cpo.mma
-Relations/Rstar.mma Coq.ma
+Relations/Rstar.mma Coq.ma Init/Prelude.ma
 Reals/Reals.mma Coq.ma Reals/Integration.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
 IntMap/Mapcanon.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
 Bool/Sumbool.ma Bool/Sumbool.mma