Skip to content
Snippets Groups Projects
Select Git revision
  • Subset
  • essais-8.18
  • master default protected
  • pr_no_math-comp
  • released
  • test_skolem_ko
  • PhD_HM_2024
  • 1.0
  • Bochner.1.0
  • Tonelli.1.0
  • LInt_p.1.0
11 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.015Oct1087126Sep252423222120191817161513121110865429Aug272630Jul292827262524221918171698428Jun2625212019181413111074314May13106129Apr282625242322212019152130Mar2928262522212019181615141310987654127Feb262322212019161514129876532131Jan30292827262524231817161527Dec232221201918171615141312118765432130Nov2928272624232221Fix Div0 issue:Add nat_neq_0_equiv, nat_add_sub_{l,r}Ign notation incompatible prefix.FIXME: Div0 issue!WIP: migrate FEM to Coq-8.20.Context now needs a section.WIP: migrate Lebesgue for Coq-8.20.WIP: migrate Lebesgue for Coq-8.20.intuition -> auto with real/arith/zarithRlt_Rminus -> Rlt_0_minusRm unused Even requirement.Mv extF_widenF_S from Finite_family to ord_compl.Helper.Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysisReorganize Compl.Add lex_1, colex_1.Add lex_1, colex_1.Fix doc.weighted orders, preuve de lexmodify the proof of unisolvence_cur.Change in indices.rename: node_cur_aux -> node_cur_alt.rename:Use new API (from Binary_relation) -> fix all *lex_* results.Maj doc.Add *lexF_{asym,str_conn},Fix {lex,colex}_trans.logic_compl:Lemmes faciles explicitésrenommagegraded_involutiveRm useless.Rename {comp,incomp} -> {compar,incompar}.Mv stuff around.logic_compl:Rename bin_rel_* -> br_*,logic_compl:Add doc.Add some doc.Extract generic binary relation stuff