we always save the discharged object for future reference

diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli
index d1a07a4ede269ef40ff4c1a00e6faf6a8b0c3b6a..c868bc61546c15db95af35b56e9a5f1ff2d63680 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.mli
+++ b/helm/software/components/grafite_engine/grafiteEngine.mli
@@ -56,3 +56,5 @@ val eval_ast :
   disambiguator_input ->
    (* the new status and generated objects, if any *)
    GrafiteTypes.status * UriManager.uri list
+
+val refinement_toolkit: RefinementTool.kit

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index f58f4dae2e1cba819e7eb1795df1d74d136b8a5b..58fc1920813ae09291d52d7e4285ec0eb5b2552f 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -41,6 +41,9 @@ module Un = CicUniv
 module E  = CicEnvironment
 module TC = CicTypeChecker
 module G  = GrafiteAst
+module GE = GrafiteEngine
+module LS = LibrarySync
+module Ds = CicDischarge
 
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
@@ -215,8 +218,16 @@ let txt_of_cic_object
         "\n\n" ^ String.concat "" (List.map aux script)
 
 let cic_prefix = Str.regexp_string "cic:/"
-
 let matita_prefix = Str.regexp_string "cic:/matita/"
+let suffixes = [".ind"; "_rec.con"; "_rect.con"; "_ind.con"; ".con"]
+
+let replacements = 
+   let map s = String.length s, s, Str.regexp_string s, "_discharged" ^ s in 
+   List.map map suffixes
+
+let replacement (ok, u) (l, s, x, t) =
+   if ok then ok, u else
+   if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u
 
 let discharge_uri style uri =
    let template = match style with
@@ -226,6 +237,7 @@ let discharge_uri style uri =
    let s = UM.string_of_uri uri in
    if Str.string_match matita_prefix s 0 then uri else
    let s = Str.replace_first cic_prefix template s in
+   let _, s = List.fold_left replacement (false, s) replacements in 
    UM.uri_of_string s
 
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
@@ -240,14 +252,11 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
       try
 (* FG: for now the explicit variables must be discharged *)
         let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
-        match CicDischarge.discharge_uri (discharge_uri style) uri with
-          | C.InductiveDefinition _ as obj', false ->
-             let uri' = discharge_uri style uri in
-             TC.typecheck_obj uri' obj';  
-             (* we loose the sharing in this case *)
-              let obj'', _ = E.get_obj Un.default_ugraph uri' in
-             let s = do_it obj'' in begin E.remove_obj uri'; s end 
-          | obj, _                                 -> do_it obj
+        let obj, real = Ds.discharge_uri (discharge_uri style) uri in
+       if real then do_it obj else
+       let newuri = discharge_uri style uri in
+       let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
+       do_it obj
       with
          | e -> 
             let msg = 

diff --git a/helm/software/matita/contribs/procedural/Coq/depends b/helm/software/matita/contribs/procedural/Coq/depends
index 14c774443791b2d99334c507bfdbcfd7e8b2f8bd..5088e5f29fc6d365834353b7dd23a3739b395a93 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/depends
+++ b/helm/software/matita/contribs/procedural/Coq/depends
@@ -1,451 +1,395 @@
-IntMap/Addec.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma
-Reals/Rprod.mma Arith/Compare.ma Coq.ma Reals/Binomial.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
-Num/GtProps.ma Num/GtProps.mma
-Arith/Peano_dec.mma Coq.ma Logic/Decidable.ma
-Num/NeqAxioms.mma Coq.ma Num/EqParams.ma Num/NeqParams.ma
-IntMap/Addr.ma IntMap/Addr.mma
-Bool/Sumbool.ma Bool/Sumbool.mma
+Logic/Hurkens.ma Logic/Hurkens.mma
+Reals/Binomial.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma
+Sets/Finite_sets.ma Sets/Finite_sets.mma
+Logic/Classical_Pred_Type.mma Coq.ma Logic/Classical_Prop.ma
+Logic/ChoiceFacts.ma Logic/ChoiceFacts.mma
+Reals/Rgeom.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
+Logic/Classical.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma
+Lists/MonoList.mma Arith/Le.ma Coq.ma
+Init/Notations.ma Init/Notations.mma
+Reals/Ranalysis.ma Reals/Ranalysis.mma
+ZArith/ZArith.ma ZArith/ZArith.mma
+ZArith/Zwf.mma Arith/Wf_nat.ma Coq.ma ZArith/ZArith_base.ma
+Sets/Relations_2_facts.ma Sets/Relations_2_facts.mma
+Reals/Rsqrt_def.mma Bool/Sumbool.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
+Reals/Rbasic_fun.ma Reals/Rbasic_fun.mma
+Arith/Euclid.mma Arith/Compare_dec.ma Arith/Mult.ma Arith/Wf_nat.ma Coq.ma
+Arith/Minus.mma Arith/Le.ma Arith/Lt.ma Coq.ma
 Reals/Raxioms.ma Reals/Raxioms.mma
-Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Exponentiation.mma
-Num/GtAxioms.mma Coq.ma Num/Axioms.ma Num/LeProps.ma
-Num/Nat/NeqDef.mma Coq.ma Num/Params.ma
-ZArith/Zmin.mma Arith/Arith.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
-ZArith/auxiliary.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma ZArith/BinInt.ma ZArith/Zorder.ma
-Num/AddProps.mma Coq.ma Num/Axioms.ma Num/EqAxioms.ma
-Reals/RiemannInt.ma Reals/RiemannInt.mma
-Arith/Lt.mma Arith/Le.ma Coq.ma
-Arith/Max.mma Arith/Arith.ma Coq.ma
-Reals/Rtrigo_reg.mma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Num/DiscrProps.ma Num/DiscrProps.mma
-Sets/Partial_Order.ma Sets/Partial_Order.mma
-Num/NeqDef.mma Coq.ma Num/EqAxioms.ma Num/EqParams.ma Num/Params.ma
-Lists/ListSet.ma Lists/ListSet.mma
-Wellfounded/Disjoint_Union.ma Wellfounded/Disjoint_Union.mma
-Bool/Sumbool.mma Coq.ma
-Init/Datatypes.ma Init/Datatypes.mma
-Num/NeqParams.mma Coq.ma Num/Params.ma
-Arith/Div2.mma Arith/Compare_dec.ma Arith/Even.ma Arith/Lt.ma Arith/Plus.ma Coq.ma
-Reals/Rderiv.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rlimit.ma
+Init/Prelude.ma Init/Prelude.mma
+ZArith/Zorder.mma Arith/Arith.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma
+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
+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
+Arith/Between.ma Arith/Between.mma
+ZArith/Zpower.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma
+Logic/Classical_Pred_Set.ma Logic/Classical_Pred_Set.mma
+ZArith/ZArith_base.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/ZArith_dec.ma ZArith/Zabs.ma ZArith/Zbool.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zhints.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma
+Arith/Compare.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Min.ma Arith/Peano_dec.ma Arith/Wf_nat.ma Coq.ma
+Reals/Ranalysis4.mma Coq.ma Reals/Exp_prop.ma Reals/Ranalysis1.ma Reals/Ranalysis3.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
+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
 ZArith/Zpower.ma ZArith/Zpower.mma
-IntMap/Lsort.ma IntMap/Lsort.mma
-IntMap/Mapc.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/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
-Reals/Rbase.mma Coq.ma Reals/DiscrR.ma Reals/RIneq.ma Reals/Raxioms.ma Reals/Rdefinitions.ma
-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
-Num/OppAxioms.mma Coq.ma
-Wellfounded/Inclusion.ma Wellfounded/Inclusion.mma
-Logic/Classical.ma Logic/Classical.mma
-Relations/Relation_Definitions.mma Coq.ma
-Sets/Cpo.mma Coq.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma
+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
+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
+Wellfounded/Union.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
+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
+Reals/Rsigma.ma Reals/Rsigma.mma
+Bool/BoolEq.ma Bool/BoolEq.mma
+Wellfounded/Disjoint_Union.ma Wellfounded/Disjoint_Union.mma
+Wellfounded/Inverse_Image.ma Wellfounded/Inverse_Image.mma
+Reals/R_sqrt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma
+Bool/BoolEq.mma Bool/Bool.ma Coq.ma
+Lists/List.mma Arith/Le.ma Coq.ma
+Reals/Rsigma.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
+Logic/ClassicalDescription.mma Coq.ma Logic/Classical.ma
 Reals/Ranalysis1.ma Reals/Ranalysis1.mma
-Logic/Classical.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma
-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
+Wellfounded/Transitive_Closure.ma Wellfounded/Transitive_Closure.mma
+ZArith/ZArith_base.ma ZArith/ZArith_base.mma
+Logic/Classical_Pred_Set.mma Coq.ma Logic/Classical_Prop.ma
+ZArith/Zeven.ma ZArith/Zeven.mma
+Init/Logic_Type.ma Init/Logic_Type.mma
+Relations/Operators_Properties.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
+Bool/DecBool.ma Bool/DecBool.mma
 Reals/Rtopology.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/RList.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Logic/ClassicalFacts.ma Logic/ClassicalFacts.mma
-Reals/ArithProp.ma Reals/ArithProp.mma
-Relations/Newman.mma Coq.ma Relations/Rstar.ma
-ZArith/Zorder.ma ZArith/Zorder.mma
-Init/Peano.ma Init/Peano.mma
-Wellfounded/Wellfounded.mma Coq.ma Wellfounded/Disjoint_Union.ma Wellfounded/Inclusion.ma Wellfounded/Inverse_Image.ma Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Product.ma Wellfounded/Transitive_Closure.ma Wellfounded/Union.ma Wellfounded/Well_Ordering.ma
-IntMap/Addr.mma Bool/Bool.ma Coq.ma ZArith/ZArith.ma
-Num/LeProps.mma Coq.ma Num/LeAxioms.ma Num/LtProps.ma
-Arith/Compare_dec.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Decidable.ma
-Sets/Integers.mma Arith/Compare_dec.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Infinite_sets.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma Sets/Relations_1.ma
-Reals/DiscrR.mma Coq.ma Reals/RIneq.ma
-IntMap/Fset.ma IntMap/Fset.mma
-Reals/Integration.ma Reals/Integration.mma
+Arith/EqNat.ma Arith/EqNat.mma
+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
+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
+Arith/Peano_dec.mma Coq.ma Logic/Decidable.ma
+Reals/PartSum.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rseries.ma
+Reals/Rtrigo_fun.ma Reals/Rtrigo_fun.mma
+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
+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
+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
+Reals/Rtrigo_fun.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
+Init/Wf.ma Init/Wf.mma
 Reals/Rtrigo_alt.ma Reals/Rtrigo_alt.mma
-Init/Notations.ma Init/Notations.mma
-NArith/BinNat.mma Coq.ma NArith/BinPos.ma
-Reals/Ranalysis4.ma Reals/Ranalysis4.mma
-Reals/Rseries.mma Arith/Compare.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Arith/Factorial.mma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma
-Sets/Classical_sets.ma Sets/Classical_sets.mma
-Reals/RList.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Reals/DiscrR.ma Reals/DiscrR.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/Cos_rel.ma Reals/Cos_rel.mma
+Logic/Classical_Prop.mma Coq.ma Logic/ProofIrrelevance.ma
+IntMap/Adist.ma IntMap/Adist.mma
+Reals/PartSum.ma Reals/PartSum.mma
+Reals/Rdefinitions.ma Reals/Rdefinitions.mma
 Sets/Relations_1_facts.mma Coq.ma Sets/Relations_1.ma
-Reals/Rtrigo_reg.ma Reals/Rtrigo_reg.mma
-ZArith/ZArith.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zbool.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma ZArith/Zlogarithm.ma ZArith/Zpower.ma ZArith/Zsqrt.ma
-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
-ZArith/Zlogarithm.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zpower.ma
+Reals/Exp_prop.ma Reals/Exp_prop.mma
+Reals/Rfunctions.mma Coq.ma Reals/ArithProp.ma Reals/R_Ifp.ma Reals/R_sqr.ma Reals/Rbase.ma Reals/Rbasic_fun.ma Reals/SplitAbsolu.ma Reals/SplitRmult.ma ZArith/Zpower.ma
+Logic/ProofIrrelevance.mma Coq.ma Logic/Hurkens.ma
+Wellfounded/Well_Ordering.ma Wellfounded/Well_Ordering.mma
+Reals/Rtrigo_reg.mma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
+Reals/Rseries.ma Reals/Rseries.mma
+Logic/Eqdep.ma Logic/Eqdep.mma
+Reals/Raxioms.mma Coq.ma Reals/Rdefinitions.ma ZArith/ZArith_base.ma
+ZArith/Zwf.ma ZArith/Zwf.mma
+ZArith/Zabs.mma Arith/Arith.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zorder.ma
+ZArith/Zmin.mma Arith/Arith.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
+Reals/Rsqrt_def.ma Reals/Rsqrt_def.mma
+Reals/R_sqrt.ma Reals/R_sqrt.mma
+Sets/Finite_sets_facts.ma Sets/Finite_sets_facts.mma
+Reals/Rbasic_fun.mma Coq.ma Reals/R_Ifp.ma Reals/Rbase.ma
+Reals/Ranalysis2.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma
+Arith/Between.mma Arith/Le.ma Arith/Lt.ma Coq.ma
+Init/Peano.ma Init/Peano.mma
+Arith/Plus.ma Arith/Plus.mma
+Setoids/Setoid.ma Setoids/Setoid.mma
+Reals/AltSeries.ma Reals/AltSeries.mma
+Reals/Rprod.ma Reals/Rprod.mma
+Sets/Permut.ma Sets/Permut.mma
+Sets/Relations_3.ma Sets/Relations_3.mma
 Reals/Rtopology.ma Reals/Rtopology.mma
-Reals/Rtrigo_fun.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
-Sets/Ensembles.ma Sets/Ensembles.mma
-Reals/Rdefinitions.ma Reals/Rdefinitions.mma
-Num/GtProps.mma Coq.ma
-ZArith/Zmisc.ma ZArith/Zmisc.mma
-Sets/Relations_1.ma Sets/Relations_1.mma
-Reals/Alembert.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
+Relations/Relations.ma Relations/Relations.mma
+IntMap/Map.ma IntMap/Map.mma
+IntMap/Mapsubset.ma IntMap/Mapsubset.mma
+ZArith/BinInt.mma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinNat.ma NArith/BinPos.ma NArith/Pnat.ma
 Sets/Powerset.ma Sets/Powerset.mma
-ZArith/Zcompare.ma ZArith/Zcompare.mma
-Sets/Finite_sets_facts.ma Sets/Finite_sets_facts.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/Mult.ma Arith/Mult.mma
+Reals/R_Ifp.mma Coq.ma Reals/Rbase.ma
+Reals/Rderiv.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rlimit.ma
+Sets/Powerset_Classical_facts.ma Sets/Powerset_Classical_facts.mma
+Sets/Uniset.mma Bool/Bool.ma Coq.ma Sets/Permut.ma
+Lists/List.ma Lists/List.mma
+ZArith/ZArith_dec.ma ZArith/ZArith_dec.mma
+IntMap/Mapcanon.ma IntMap/Mapcanon.mma
+IntMap/Allmaps.ma IntMap/Allmaps.mma
 Wellfounded/Lexicographic_Exponentiation.mma Coq.ma Lists/List.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
-Logic/ChoiceFacts.ma Logic/ChoiceFacts.mma
-Num/EqParams.ma Num/EqParams.mma
+Sets/Powerset_facts.mma Coq.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
+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
+Reals/Rdefinitions.mma Coq.ma ZArith/ZArith_base.ma
+Reals/PSeries_reg.ma Reals/PSeries_reg.mma
+IntMap/Adalloc.ma IntMap/Adalloc.mma
+Reals/R_Ifp.ma Reals/R_Ifp.mma
+Logic/Classical_Prop.ma Logic/Classical_Prop.mma
 IntMap/Mapiter.mma 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 Lists/List.ma ZArith/ZArith.ma
-Reals/PartSum.ma Reals/PartSum.mma
-Num/Definitions.mma Coq.ma
-Num/DiscrAxioms.mma Coq.ma Num/NSyntax.ma Num/Params.ma
-ZArith/Zsqrt.mma Coq.ma ZArith/ZArith_base.ma
-Reals/Rderiv.ma Reals/Rderiv.mma
-Wellfounded/Union.ma Wellfounded/Union.mma
-Arith/Gt.mma Arith/Le.ma Arith/Lt.ma Arith/Plus.ma Coq.ma
-Arith/Even.ma Arith/Even.mma
+Wellfounded/Inclusion.ma Wellfounded/Inclusion.mma
+ZArith/auxiliary.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma ZArith/BinInt.ma ZArith/Zorder.ma
+Reals/RIneq.ma Reals/RIneq.mma
+Init/Logic.mma Coq.ma Init/Notations.ma
+Lists/ListSet.ma Lists/ListSet.mma
+Relations/Relation_Definitions.ma Relations/Relation_Definitions.mma
+Wellfounded/Disjoint_Union.mma Coq.ma Relations/Relation_Operators.ma
+Sets/Finite_sets_facts.mma Arith/Gt.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
+Arith/Div2.mma Arith/Compare_dec.ma Arith/Even.ma Arith/Lt.ma Arith/Plus.ma Coq.ma
+Init/Notations.mma Coq.ma
+Sorting/Permutation.ma Sorting/Permutation.mma
+Arith/Bool_nat.mma Arith/Compare_dec.ma Arith/Peano_dec.ma Bool/Sumbool.ma Coq.ma
+Arith/Min.ma Arith/Min.mma
+IntMap/Mapfold.mma 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/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
+Logic/RelationalChoice.ma Logic/RelationalChoice.mma
+Reals/ArithProp.ma Reals/ArithProp.mma
+Reals/Rprod.mma Arith/Compare.ma Coq.ma Reals/Binomial.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
+Sets/Constructive_sets.ma Sets/Constructive_sets.mma
 Sets/Constructive_sets.mma Coq.ma Sets/Ensembles.ma
-Reals/Rseries.ma Reals/Rseries.mma
-Arith/Minus.ma Arith/Minus.mma
-Lists/List.mma Arith/Le.ma Coq.ma
-ZArith/ZArith_base.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/ZArith_dec.ma ZArith/Zabs.ma ZArith/Zbool.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zhints.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma
-Num/Axioms.ma Num/Axioms.mma
+Logic/Diaconescu.mma Bool/Bool.ma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalFacts.ma
+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
+Lists/Streams.ma Lists/Streams.mma
+NArith/NArith.ma NArith/NArith.mma
+Relations/Newman.ma Relations/Newman.mma
 Reals/SplitRmult.ma Reals/SplitRmult.mma
-Reals/Rsqrt_def.ma Reals/Rsqrt_def.mma
-Arith/Plus.mma Arith/Le.ma Arith/Lt.ma Coq.ma
-IntMap/Map.ma IntMap/Map.mma
-Init/Logic_Type.mma Coq.ma Init/Datatypes.ma Init/Logic.ma
-Reals/Raxioms.mma Coq.ma Reals/Rdefinitions.ma ZArith/ZArith_base.ma
+Arith/Arith.mma Arith/Between.ma Arith/Compare_dec.ma Arith/Factorial.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Peano_dec.ma Arith/Plus.ma Coq.ma
+Reals/Ranalysis4.ma Reals/Ranalysis4.mma
+Reals/Rbase.ma Reals/Rbase.mma
+Arith/Lt.ma Arith/Lt.mma
+Arith/Gt.ma Arith/Gt.mma
+Bool/Bool.ma Bool/Bool.mma
+Bool/Zerob.ma Bool/Zerob.mma
+ZArith/Znumtheory.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma
+Arith/Factorial.ma Arith/Factorial.mma
+IntMap/Map.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma ZArith/ZArith.ma
+Reals/Rfunctions.ma Reals/Rfunctions.mma
+ZArith/Zmisc.ma ZArith/Zmisc.mma
 ZArith/BinInt.ma ZArith/BinInt.mma
-Reals/Rtrigo.ma Reals/Rtrigo.mma
-Reals/Ranalysis1.mma Coq.ma Reals/Rbase.ma Reals/Rderiv.ma Reals/Rfunctions.ma Reals/Rlimit.ma
-Reals/Cos_plus.ma Reals/Cos_plus.mma
+ZArith/Zcompare.ma ZArith/Zcompare.mma
+Reals/Sqrt_reg.ma Reals/Sqrt_reg.mma
+Reals/SeqSeries.ma Reals/SeqSeries.mma
+IntMap/Mapc.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/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
 Bool/Bvector.ma Bool/Bvector.mma
-Logic/Hurkens.mma Coq.ma
-Num/OppAxioms.ma Num/OppAxioms.mma
-Relations/Relations.mma Coq.ma Relations/Operators_Properties.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
-Reals/R_sqr.mma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma
-Arith/Peano_dec.ma Arith/Peano_dec.mma
-Reals/Rprod.ma Reals/Rprod.mma
-Num/NeqDef.ma Num/NeqDef.mma
-Arith/Bool_nat.mma Arith/Compare_dec.ma Arith/Peano_dec.ma Bool/Sumbool.ma Coq.ma
-ZArith/ZArith_dec.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
-Arith/Euclid.mma Arith/Compare_dec.ma Arith/Mult.ma Arith/Wf_nat.ma Coq.ma
-ZArith/Zbinary.ma ZArith/Zbinary.mma
-Logic/Decidable.ma Logic/Decidable.mma
-Logic/RelationalChoice.mma Coq.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
-Init/Prelude.ma Init/Prelude.mma
-Num/Nat/Axioms.mma Coq.ma Num/EqAxioms.ma Num/NSyntax.ma Num/Params.ma
-Reals/Rsigma.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
-ZArith/Zbinary.mma Bool/Bvector.ma Coq.ma ZArith/ZArith.ma ZArith/Zpower.ma
-Sets/Ensembles.mma Coq.ma
-Reals/Binomial.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Logic/ClassicalChoice.mma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalDescription.ma Logic/RelationalChoice.ma
-Reals/R_Ifp.ma Reals/R_Ifp.mma
-Logic/ProofIrrelevance.ma Logic/ProofIrrelevance.mma
-Reals/MVT.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtopology.ma
-Reals/RiemannInt_SF.ma Reals/RiemannInt_SF.mma
-Num/Axioms.mma Coq.ma Num/EqParams.ma Num/NSyntax.ma Num/Params.ma
-ZArith/Zdiv.ma ZArith/Zdiv.mma
-Num/GeAxioms.mma Coq.ma Num/Axioms.ma Num/LtProps.ma
-Sets/Permut.ma Sets/Permut.mma
-Num/DiscrAxioms.ma Num/DiscrAxioms.mma
-Sets/Cpo.ma Sets/Cpo.mma
-Reals/Rtrigo_calc.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Arith/Even.mma Coq.ma
-Reals/Sqrt_reg.mma Coq.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma
-ZArith/Zabs.ma ZArith/Zabs.mma
-Sorting/Heap.ma Sorting/Heap.mma
-Reals/Ranalysis3.mma Coq.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Num/Params.mma Coq.ma
-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
-Logic/Classical_Pred_Set.ma Logic/Classical_Pred_Set.mma
-Logic/Classical_Type.ma Logic/Classical_Type.mma
-Init/Prelude.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma Init/Peano.ma Init/Specif.ma Init/Wf.ma
-Wellfounded/Lexicographic_Product.mma Coq.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
-Logic/Decidable.mma Coq.ma
-Reals/Reals.mma Coq.ma Reals/Integration.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Num/Leibniz/Params.ma Num/Leibniz/Params.mma
-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
+Reals/Exp_prop.mma Arith/Div2.ma Arith/Even.ma Arith/Max.ma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
+ZArith/Zlogarithm.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zpower.ma
+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
-IntMap/Allmaps.ma IntMap/Allmaps.mma
-ZArith/Zhints.ma ZArith/Zhints.mma
-Sets/Constructive_sets.ma Sets/Constructive_sets.mma
-ZArith/Zeven.mma Coq.ma ZArith/BinInt.ma
-Num/GeAxioms.ma Num/GeAxioms.mma
-Num/Params.ma Num/Params.mma
-Reals/Rdefinitions.mma Coq.ma ZArith/ZArith_base.ma
-Reals/Rsigma.ma Reals/Rsigma.mma
+Bool/DecBool.mma Coq.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
-Reals/RIneq.mma Coq.ma Reals/Raxioms.ma
-Sets/Multiset.mma Arith/Plus.ma Coq.ma Sets/Permut.ma
-Coq.ma preamble.ma
-Relations/Relation_Operators.mma Coq.ma Lists/List.ma Relations/Relation_Definitions.ma
-Num/LeAxioms.mma Coq.ma Num/Axioms.ma Num/LtProps.ma
-Init/Wf.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
-Logic/Berardi.mma Coq.ma
-Logic/JMeq.ma Logic/JMeq.mma
-ZArith/Zmisc.mma Bool/Bool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
-Arith/Minus.mma Arith/Le.ma Arith/Lt.ma Coq.ma
-Arith/Le.ma Arith/Le.mma
-Num/AddProps.ma Num/AddProps.mma
-IntMap/Addec.ma IntMap/Addec.mma
-Logic/ClassicalFacts.mma Coq.ma
-Sets/Integers.ma Sets/Integers.mma
-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
-ZArith/ZArith.ma ZArith/ZArith.mma
-Num/LeProps.ma Num/LeProps.mma
-Num/Nat/NSyntax.mma Coq.ma
-Reals/ArithProp.mma Arith/Div2.ma Arith/Even.ma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.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
+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
+Sets/Relations_1_facts.ma Sets/Relations_1_facts.mma
+Arith/Div2.ma Arith/Div2.mma
+Wellfounded/Lexicographic_Product.ma Wellfounded/Lexicographic_Product.mma
+Init/Peano.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
 Logic/Berardi.ma Logic/Berardi.mma
-Num/OppProps.mma Coq.ma
-Relations/Rstar.mma Coq.ma
+Init/Datatypes.ma Init/Datatypes.mma
 Reals/SplitRmult.mma Coq.ma Reals/Rbase.ma
-IntMap/Mapsubset.ma IntMap/Mapsubset.mma
-Arith/Div.mma Arith/Compare_dec.ma Arith/Le.ma Coq.ma
-Bool/Zerob.ma Bool/Zerob.mma
-Wellfounded/Well_Ordering.ma Wellfounded/Well_Ordering.mma
-Reals/Rsqrt_def.mma Bool/Sumbool.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
-Reals/Ranalysis2.ma Reals/Ranalysis2.mma
-Reals/R_sqrt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma
-Sorting/Permutation.ma Sorting/Permutation.mma
-Reals/Rlimit.ma Reals/Rlimit.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
-Arith/Compare.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Min.ma Arith/Peano_dec.ma Arith/Wf_nat.ma Coq.ma
-Sets/Finite_sets.ma Sets/Finite_sets.mma
-Relations/Newman.ma Relations/Newman.mma
-NArith/NArith.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma
-Lists/List.ma Lists/List.mma
-ZArith/ZArith_base.ma ZArith/ZArith_base.mma
-Sets/Infinite_sets.ma Sets/Infinite_sets.mma
-Reals/Alembert.ma Reals/Alembert.mma
-Sets/Relations_1.mma Coq.ma
-ZArith/ZArith_dec.ma ZArith/ZArith_dec.mma
-Bool/Bool.mma Coq.ma
-ZArith/Zcompare.mma Arith/Gt.ma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma
-Reals/NewtonInt.ma Reals/NewtonInt.mma
-Num/DiscrProps.mma Coq.ma Num/DiscrAxioms.ma Num/LtProps.ma
-Sorting/Heap.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma Sorting/Sorting.ma
-Reals/R_sqrt.ma Reals/R_sqrt.mma
-Sets/Powerset_facts.ma Sets/Powerset_facts.mma
-Reals/Rfunctions.ma Reals/Rfunctions.mma
-Bool/IfProp.ma Bool/IfProp.mma
-Relations/Operators_Properties.ma Relations/Operators_Properties.mma
-Reals/NewtonInt.mma Coq.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-ZArith/Zcomplements.mma Arith/Wf_nat.ma Coq.ma Lists/List.ma ZArith/ZArith_base.ma
-Bool/Zerob.mma Arith/Arith.ma Bool/Bool.ma Coq.ma
 Sets/Relations_2.ma Sets/Relations_2.mma
-Init/Specif.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
-ZArith/Zabs.mma Arith/Arith.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zorder.ma
-Logic/Eqdep.ma Logic/Eqdep.mma
-Bool/BoolEq.ma Bool/BoolEq.mma
-ZArith/Zlogarithm.ma ZArith/Zlogarithm.mma
-NArith/BinNat.ma NArith/BinNat.mma
-Reals/MVT.ma Reals/MVT.mma
-Lists/MonoList.mma Arith/Le.ma Coq.ma
-NArith/NArith.ma NArith/NArith.mma
-Num/GeProps.ma Num/GeProps.mma
-Arith/Between.ma Arith/Between.mma
-Num/GeProps.mma Coq.ma
-preamble.ma coq.ma
-Reals/PSeries_reg.ma Reals/PSeries_reg.mma
-Num/SubProps.ma Num/SubProps.mma
-Num/Leibniz/NSyntax.ma Num/Leibniz/NSyntax.mma
-NArith/BinPos.ma NArith/BinPos.mma
-Reals/AltSeries.ma Reals/AltSeries.mma
-Reals/SeqProp.mma Arith/Max.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
-Logic/ClassicalDescription.ma Logic/ClassicalDescription.mma
-IntMap/Mapcanon.ma IntMap/Mapcanon.mma
-Reals/Rgeom.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Wellfounded/Transitive_Closure.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
-Sets/Relations_3.mma Coq.ma Sets/Relations_1.ma Sets/Relations_2.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
-Arith/Lt.ma Arith/Lt.mma
 Reals/RList.ma Reals/RList.mma
-Arith/Between.mma Arith/Le.ma Arith/Lt.ma Coq.ma
-Num/Definitions.ma Num/Definitions.mma
-Arith/Plus.ma Arith/Plus.mma
-Reals/R_sqr.ma Reals/R_sqr.mma
-Init/Peano.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma
-Logic/Classical_Pred_Type.mma Coq.ma Logic/Classical_Prop.ma
-Reals/Binomial.ma Reals/Binomial.mma
-Arith/Min.mma Arith/Arith.ma Coq.ma
-Relations/Relation_Operators.ma Relations/Relation_Operators.mma
-Reals/RIneq.ma Reals/RIneq.mma
-Lists/MonoList.ma Lists/MonoList.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
-Arith/Min.ma Arith/Min.mma
-Reals/PSeries_reg.mma Arith/Even.ma Arith/Max.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
-Reals/Rtrigo_def.ma Reals/Rtrigo_def.mma
-IntMap/Adalloc.ma IntMap/Adalloc.mma
-Wellfounded/Well_Ordering.mma Coq.ma Logic/Eqdep.ma
-IntMap/Map.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma ZArith/ZArith.ma
-Reals/SplitAbsolu.ma Reals/SplitAbsolu.mma
-Arith/Compare_dec.ma Arith/Compare_dec.mma
-Arith/Euclid.ma Arith/Euclid.mma
-Arith/EqNat.ma Arith/EqNat.mma
-Num/SubProps.mma Coq.ma
-Lists/ListSet.mma Coq.ma Lists/List.ma
-Sets/Finite_sets_facts.mma Arith/Gt.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma
-IntMap/Mapfold.mma 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/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
-ZArith/Zorder.mma Arith/Arith.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma
-Logic/Classical_Pred_Set.mma Coq.ma Logic/Classical_Prop.ma
-Num/Leibniz/NSyntax.mma Coq.ma Num/Params.ma
-Sets/Relations_2_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma
-Reals/Integration.mma Coq.ma Reals/NewtonInt.ma Reals/RiemannInt.ma Reals/RiemannInt_SF.ma
-Sets/Partial_Order.mma Coq.ma Sets/Ensembles.ma Sets/Relations_1.ma
-Reals/Rfunctions.mma Coq.ma Reals/ArithProp.ma Reals/R_Ifp.ma Reals/R_sqr.ma Reals/Rbase.ma Reals/Rbasic_fun.ma Reals/SplitAbsolu.ma Reals/SplitRmult.ma ZArith/Zpower.ma
-IntMap/Mapcard.ma IntMap/Mapcard.mma
-Arith/Arith.ma Arith/Arith.mma
-Arith/Max.ma Arith/Max.mma
-Reals/Exp_prop.mma Arith/Div2.ma Arith/Even.ma Arith/Max.ma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Reals/Rbase.ma Reals/Rbase.mma
-Bool/IfProp.mma Bool/Bool.ma Coq.ma
-ZArith/BinInt.mma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinNat.ma NArith/BinPos.ma NArith/Pnat.ma
-Num/Nat/Axioms.ma Num/Nat/Axioms.mma
-Relations/Relations.ma Relations/Relations.mma
-ZArith/Zeven.ma ZArith/Zeven.mma
-ZArith/Zbool.ma ZArith/Zbool.mma
-Init/Wf.ma Init/Wf.mma
-Reals/R_Ifp.mma Coq.ma Reals/Rbase.ma
-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
-Sets/Powerset_facts.mma Coq.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma
-Init/Datatypes.mma Coq.ma Init/Logic.ma Init/Notations.ma
-Logic/Diaconescu.mma Bool/Bool.ma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalFacts.ma
-IntMap/Mapaxioms.mma 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
-Arith/Mult.mma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Plus.ma Coq.ma
-Logic/Classical_Prop.mma Coq.ma Logic/ProofIrrelevance.ma
-Num/Leibniz/EqAxioms.mma Coq.ma Num/NSyntax.ma
-Num/Nat/NeqDef.ma Num/Nat/NeqDef.mma
-Logic/ProofIrrelevance.mma Coq.ma Logic/Hurkens.ma
-ZArith/auxiliary.ma ZArith/auxiliary.mma
+Arith/Max.mma Arith/Arith.ma Coq.ma
+preamble.ma coq.ma
+ZArith/Zorder.ma ZArith/Zorder.mma
 Sets/Image.ma Sets/Image.mma
-Num/NeqAxioms.ma Num/NeqAxioms.mma
+NArith/BinPos.ma NArith/BinPos.mma
+ZArith/Zcomplements.ma ZArith/Zcomplements.mma
 Reals/Rtrigo_def.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_fun.ma Reals/SeqSeries.ma
-Relations/Operators_Properties.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
+Reals/PSeries_reg.mma Arith/Even.ma Arith/Max.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma
+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
+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
+Bool/IfProp.ma Bool/IfProp.mma
+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
+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
+IntMap/Maplists.ma IntMap/Maplists.mma
+Arith/Bool_nat.ma Arith/Bool_nat.mma
+Logic/JMeq.ma Logic/JMeq.mma
+Reals/DiscrR.mma Coq.ma Reals/RIneq.ma
+IntMap/Mapc.ma IntMap/Mapc.mma
 IntMap/Maplists.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapc.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapfold.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma
-Num/OppProps.ma Num/OppProps.mma
-Logic/ClassicalChoice.ma Logic/ClassicalChoice.mma
-Reals/RiemannInt_SF.mma Coq.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Num/LtProps.mma Coq.ma Num/AddProps.ma Num/Axioms.ma Num/NeqProps.ma
-Reals/SeqProp.ma Reals/SeqProp.mma
-Reals/SeqSeries.ma Reals/SeqSeries.mma
-Bool/DecBool.mma Coq.ma
-Init/Specif.ma Init/Specif.mma
-Init/Logic.mma Coq.ma Init/Notations.ma
-Logic/Classical_Prop.ma Logic/Classical_Prop.mma
-Setoids/Setoid.ma Setoids/Setoid.mma
-IntMap/Mapfold.ma IntMap/Mapfold.mma
-Logic/Classical_Type.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma
-Setoids/Setoid.mma Coq.ma
-Init/Logic.ma Init/Logic.mma
-IntMap/Adist.ma IntMap/Adist.mma
-ZArith/Wf_Z.ma ZArith/Wf_Z.mma
-Sets/Uniset.ma Sets/Uniset.mma
+Sets/Relations_3.mma Coq.ma Sets/Relations_1.ma Sets/Relations_2.ma
+Arith/Peano_dec.ma Arith/Peano_dec.mma
+IntMap/Mapaxioms.ma IntMap/Mapaxioms.mma
+Reals/Binomial.ma Reals/Binomial.mma
 Logic/Eqdep_dec.ma Logic/Eqdep_dec.mma
-Sorting/Sorting.ma Sorting/Sorting.mma
-Reals/Cauchy_prod.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma
-ZArith/Zsqrt.ma ZArith/Zsqrt.mma
-Reals/Ranalysis2.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma
+Init/Datatypes.mma Coq.ma Init/Logic.ma Init/Notations.ma
+Wellfounded/Inclusion.mma Coq.ma Relations/Relation_Definitions.ma
+Sets/Infinite_sets.ma Sets/Infinite_sets.mma
+Sets/Multiset.mma Arith/Plus.ma Coq.ma Sets/Permut.ma
+Logic/Classical.ma Logic/Classical.mma
+IntMap/Mapaxioms.mma 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
 IntMap/Mapiter.ma IntMap/Mapiter.mma
-Logic/Hurkens.ma Logic/Hurkens.mma
-Sets/Relations_3_facts.ma Sets/Relations_3_facts.mma
-ZArith/Zwf.mma Arith/Wf_nat.ma Coq.ma ZArith/ZArith_base.ma
-Reals/AltSeries.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
-Logic/RelationalChoice.ma Logic/RelationalChoice.mma
+Reals/SplitAbsolu.ma Reals/SplitAbsolu.mma
 Reals/Ranalysis3.ma Reals/Ranalysis3.mma
-IntMap/Fset.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Map.ma ZArith/ZArith.ma
-IntMap/Adist.mma Arith/Arith.ma Arith/Min.ma Bool/Bool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma
-Arith/Compare.ma Arith/Compare.mma
-Reals/Rtrigo_alt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
-ZArith/Wf_Z.mma Arith/Wf_nat.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma
-Wellfounded/Disjoint_Union.mma Coq.ma Relations/Relation_Operators.ma
-Sets/Uniset.mma Bool/Bool.ma Coq.ma Sets/Permut.ma
-Sets/Relations_2_facts.ma Sets/Relations_2_facts.mma
-Num/NSyntax.mma Coq.ma Num/Params.ma
-Arith/Wf_nat.ma Arith/Wf_nat.mma
-Reals/Rcomplete.ma Reals/Rcomplete.mma
-Reals/Rtrigo.mma Coq.ma Logic/Classical_Prop.ma Reals/Cos_plus.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_alt.ma Reals/Rtrigo_def.ma Reals/Rtrigo_fun.ma Reals/SeqSeries.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma
+Logic/ChoiceFacts.mma Coq.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
-ZArith/Znumtheory.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zdiv.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/Rtrigo_fun.ma Reals/Rtrigo_fun.mma
-Wellfounded/Wellfounded.ma Wellfounded/Wellfounded.mma
-Arith/Bool_nat.ma Arith/Bool_nat.mma
-Sets/Relations_1_facts.ma Sets/Relations_1_facts.mma
-Arith/Gt.ma Arith/Gt.mma
-Reals/Rtrigo_calc.ma Reals/Rtrigo_calc.mma
-Reals/Reals.ma Reals/Reals.mma
-Num/Nat/NSyntax.ma Num/Nat/NSyntax.mma
-Sets/Relations_3.ma Sets/Relations_3.mma
-Reals/Exp_prop.ma Reals/Exp_prop.mma
-Num/EqAxioms.mma Coq.ma Num/EqParams.ma Num/NSyntax.ma Num/Params.ma
-Num/Leibniz/EqAxioms.ma Num/Leibniz/EqAxioms.mma
-Num/NSyntax.ma Num/NSyntax.mma
-Num/NeqProps.ma Num/NeqProps.mma
+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
-ZArith/Zpower.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.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
+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
+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
+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
+Bool/Zerob.mma Arith/Arith.ma Bool/Bool.ma Coq.ma
+ZArith/Znumtheory.ma ZArith/Znumtheory.mma
+Reals/R_sqr.ma Reals/R_sqr.mma
+ZArith/Zdiv.ma ZArith/Zdiv.mma
+Relations/Relations.mma Coq.ma Relations/Operators_Properties.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma
 IntMap/Mapcard.mma Arith/Arith.ma Arith/Peano_dec.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/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma
-Reals/Ranalysis.ma Reals/Ranalysis.mma
+Reals/Rtrigo.mma Coq.ma Logic/Classical_Prop.ma Reals/Cos_plus.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_alt.ma Reals/Rtrigo_def.ma Reals/Rtrigo_fun.ma Reals/SeqSeries.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma
+Arith/Factorial.mma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma
+Sorting/Heap.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma Sorting/Sorting.ma
+Sets/Cpo.mma Coq.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma
+Reals/Sqrt_reg.mma Coq.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma
+Init/Logic_Type.mma Coq.ma Init/Datatypes.ma Init/Logic.ma
+Relations/Relation_Operators.ma Relations/Relation_Operators.mma
+Arith/Plus.mma Arith/Le.ma Arith/Lt.ma Coq.ma
+Arith/Gt.mma Arith/Le.ma Arith/Lt.ma Arith/Plus.ma Coq.ma
+Init/Specif.ma Init/Specif.mma
+Relations/Newman.mma Coq.ma Relations/Rstar.ma
 IntMap/Lsort.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Map.ma IntMap/Mapiter.ma Lists/List.ma ZArith/ZArith.ma
-ZArith/Znumtheory.ma ZArith/Znumtheory.mma
-Reals/Ranalysis4.mma Coq.ma Reals/Exp_prop.ma Reals/Ranalysis1.ma Reals/Ranalysis3.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
-Num/NeqParams.ma Num/NeqParams.mma
-ZArith/Zmin.ma ZArith/Zmin.mma
-Sets/Classical_sets.mma Coq.ma Logic/Classical_Type.ma Sets/Constructive_sets.ma Sets/Ensembles.ma
-Arith/Wf_nat.mma Arith/Lt.ma Coq.ma
+Arith/Mult.mma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Plus.ma Coq.ma
+Arith/Max.ma Arith/Max.mma
+Sets/Relations_1.ma Sets/Relations_1.mma
+Reals/RList.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma
+Reals/Rpower.ma Reals/Rpower.mma
+ZArith/Zdiv.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zbool.ma ZArith/Zcomplements.ma
+Reals/RiemannInt_SF.mma Coq.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma
+IntMap/Addr.ma IntMap/Addr.mma
+Arith/Compare_dec.ma Arith/Compare_dec.mma
 Lists/TheoryList.mma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Bool/DecBool.ma Coq.ma Lists/List.ma
-Sets/Finite_sets.mma Coq.ma Sets/Constructive_sets.ma Sets/Ensembles.ma
-Num/NeqProps.mma Coq.ma Num/EqAxioms.ma Num/EqParams.ma Num/NeqAxioms.ma Num/NeqParams.ma
-Sets/Powerset_Classical_facts.ma Sets/Powerset_Classical_facts.mma
-Reals/Rbasic_fun.mma Coq.ma Reals/R_Ifp.ma Reals/Rbase.ma
-Init/Logic_Type.ma Init/Logic_Type.mma
-Sets/Permut.mma Coq.ma
-Num/EqParams.mma Coq.ma Num/Params.ma
-Logic/ClassicalDescription.mma Coq.ma Logic/Classical.ma
-Init/Notations.mma Coq.ma
-NArith/BinPos.mma Coq.ma
-Reals/PartSum.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rseries.ma
+Reals/RiemannInt_SF.ma Reals/RiemannInt_SF.mma
+Logic/Classical_Type.ma Logic/Classical_Type.mma
+Arith/Euclid.ma Arith/Euclid.mma
+Reals/Rcomplete.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
+Logic/ClassicalChoice.ma Logic/ClassicalChoice.mma
+Reals/NewtonInt.mma Coq.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.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
+IntMap/Fset.ma IntMap/Fset.mma
 Logic/JMeq.mma Coq.ma Logic/Eqdep.ma
-Wellfounded/Transitive_Closure.ma Wellfounded/Transitive_Closure.mma
-ZArith/Zdiv.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zbool.ma ZArith/Zcomplements.ma
-ZArith/Zwf.ma ZArith/Zwf.mma
-Num/LtProps.ma Num/LtProps.mma
-Lists/TheoryList.ma Lists/TheoryList.mma
-Sorting/Permutation.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma
-Reals/Rpower.ma Reals/Rpower.mma
-Wellfounded/Inverse_Image.ma Wellfounded/Inverse_Image.mma
-Reals/Rbasic_fun.ma Reals/Rbasic_fun.mma
-Arith/Div2.ma Arith/Div2.mma
-Reals/Rlimit.mma Coq.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma
-Wellfounded/Lexicographic_Product.ma Wellfounded/Lexicographic_Product.mma
-Reals/Cos_rel.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
+ZArith/Zsqrt.mma Coq.ma ZArith/ZArith_base.ma
+Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Exponentiation.mma
+Reals/Rlimit.ma Reals/Rlimit.mma
+Reals/Rtrigo_calc.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma
+IntMap/Addec.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma
+Bool/Bvector.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma
+ZArith/Zhints.ma ZArith/Zhints.mma
+Relations/Rstar.ma Relations/Rstar.mma
+Relations/Relation_Operators.mma Coq.ma Lists/List.ma Relations/Relation_Definitions.ma
+Reals/Cauchy_prod.ma Reals/Cauchy_prod.mma
+IntMap/Lsort.ma IntMap/Lsort.mma
+IntMap/Fset.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Map.ma ZArith/ZArith.ma
+ZArith/Wf_Z.mma Arith/Wf_nat.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma
 Reals/Ranalysis.mma Coq.ma Reals/Exp_prop.ma Reals/MVT.ma Reals/PSeries_reg.ma Reals/RList.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Ranalysis3.ma Reals/Ranalysis4.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rgeom.ma Reals/Rpower.ma Reals/Rsqrt_def.ma Reals/Rtopology.ma Reals/Rtrigo.ma Reals/Rtrigo_calc.ma Reals/Rtrigo_reg.ma Reals/SeqSeries.ma Reals/Sqrt_reg.ma
-Reals/SplitAbsolu.mma Coq.ma Reals/Rbasic_fun.ma
-Num/LeAxioms.ma Num/LeAxioms.mma
+Arith/Even.ma Arith/Even.mma
+Reals/Cos_rel.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
 ZArith/Znat.ma ZArith/Znat.mma
-Relations/Rstar.ma Relations/Rstar.mma
-Logic/ChoiceFacts.mma Coq.ma
-Bool/Bool.ma Bool/Bool.mma
-Wellfounded/Union.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma
-Bool/Bvector.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma
-IntMap/Mapaxioms.ma IntMap/Mapaxioms.mma
-IntMap/Maplists.ma IntMap/Maplists.mma
-Wellfounded/Inclusion.mma Coq.ma Relations/Relation_Definitions.ma
+Logic/ClassicalChoice.mma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalDescription.ma Logic/RelationalChoice.ma
+IntMap/Addec.ma IntMap/Addec.mma
+ZArith/Zbinary.mma Bool/Bvector.ma Coq.ma ZArith/ZArith.ma ZArith/Zpower.ma
+Wellfounded/Well_Ordering.mma Coq.ma Logic/Eqdep.ma
+IntMap/Addr.mma Bool/Bool.ma Coq.ma ZArith/ZArith.ma
+Sets/Partial_Order.ma Sets/Partial_Order.mma
+Reals/AltSeries.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
+Reals/Ranalysis1.mma Coq.ma Reals/Rbase.ma Reals/Rderiv.ma Reals/Rfunctions.ma Reals/Rlimit.ma
 Logic/Diaconescu.ma Logic/Diaconescu.mma
-Reals/Cos_rel.ma Reals/Cos_rel.mma
-Reals/Rcomplete.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma
-Logic/Eqdep.mma Coq.ma
-Relations/Relation_Definitions.ma Relations/Relation_Definitions.mma
-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
-Num/GtAxioms.ma Num/GtAxioms.mma
-Arith/Factorial.ma Arith/Factorial.mma
-Arith/Arith.mma Arith/Between.ma Arith/Compare_dec.ma Arith/Factorial.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Peano_dec.ma Arith/Plus.ma Coq.ma
-Wellfounded/Inverse_Image.mma Coq.ma
-IntMap/Mapc.ma IntMap/Mapc.mma
-Bool/BoolEq.mma Bool/Bool.ma Coq.ma
-Reals/Sqrt_reg.ma Reals/Sqrt_reg.mma
-Sorting/Sorting.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma
+ZArith/Zmisc.mma Bool/Bool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma
 NArith/Pnat.ma NArith/Pnat.mma
-Arith/Div.ma Arith/Div.mma
-Sets/Multiset.ma Sets/Multiset.mma
-Num/Leibniz/Params.mma Coq.ma
-Reals/Rgeom.ma Reals/Rgeom.mma
-ZArith/Zcomplements.ma ZArith/Zcomplements.mma
-Logic/Classical_Pred_Type.ma Logic/Classical_Pred_Type.mma
-Sets/Relations_2.mma Coq.ma Sets/Relations_1.ma
-Reals/Cauchy_prod.ma Reals/Cauchy_prod.mma
-Num/EqAxioms.ma Num/EqAxioms.mma
-Bool/DecBool.ma Bool/DecBool.mma
+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
+Reals/Rcomplete.ma Reals/Rcomplete.mma
+Sets/Ensembles.ma Sets/Ensembles.mma
+Logic/Decidable.mma Coq.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
+Sets/Integers.mma Arith/Compare_dec.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Infinite_sets.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma Sets/Relations_1.ma
+Init/Logic.ma Init/Logic.mma
+Sets/Classical_sets.ma Sets/Classical_sets.mma
+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
+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
+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
+Wellfounded/Wellfounded.mma Coq.ma Wellfounded/Disjoint_Union.ma Wellfounded/Inclusion.ma Wellfounded/Inverse_Image.ma Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Product.ma Wellfounded/Transitive_Closure.ma Wellfounded/Union.ma Wellfounded/Well_Ordering.ma
+ZArith/Zcomplements.mma Arith/Wf_nat.ma Coq.ma Lists/List.ma ZArith/ZArith_base.ma
+Logic/Classical_Pred_Type.ma Logic/Classical_Pred_Type.mma
+Reals/Rtrigo_alt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma
 coq.ma