Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • no_ms
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
12 results
Created with Raphaël 2.2.015Jan141311109821Dec2019181716151413121065432129Nov28272625242321201918516Oct151087126Sep252423222120191817161513121110865429Aug272630Jul292827262524221918171698428Jun2625212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221Unify doc.Update imports.Merge branch 'Alg' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis into AlgRename Subsets -> Subsets_wDep (= with dependencies).Use classic instead of classic_dec when possible.Split ssr into ssr + ssr_wMC.Rm useless.Update imports of Subsets in Lebesgue.Rename Binary_relation.compl_invol -> Binary_relation.br_compl_invol.Unify doc in Bochner.Unify doc in Lebesgue.Unify doc in Algebra.Unify doc in Requisite, Logic, Numbers and Subsets.Export module Subsets if for subset/function stuff only!Merge Function_compl into Function.Use new API (from Subset).Dispatch contents of Subset_compl into Subset + Subset_dec + Subset_charac.Avoid weird dependency.Maybe it is better there...Might be useful...Fine tune imports in Bochner.Use new import policy in Bochner + patch proofs for new subset API.WIP: use new import policy in Legesgue + patch proofs for new subset API.Merge remote-tracking branch 'origin/master' into AlgWIP: use new import policy in Legesgue + patch proofs for new subset API.More cleaning and implicitsWIP: use new import policy in Lebesgue + patch proofs for new subset API.Merge remote-tracking branch 'origin/master' into AlgUse new import policy for old subset modules.Cleaning in progressMerge branch 'Alg' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis into AlgMerge branch 'Alg' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis into AlgAdd KerS0_correct + doc.Merge remote-tracking branch 'origin/master' into AlgMaj doc.More implicitsAdd KerS0_correct + doc.Merge remote-tracking branch 'origin/master' into AlgUpdate doc in Requisite, Logic, Numbers and Algebra.Export -> Import.