aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2019-10-31Zgcd_alt: use “lia” rather than “omega”Vincent Laporte
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-28[stdlib]Reals: use “lia” rather than “omega”Vincent Laporte
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-22FSetEqProperties: do not use “omega”Vincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Qround: do not use “omega”Vincent Laporte
2019-10-22Qreduction: do not use “omega”Vincent Laporte
2019-10-22QArith_base: do not use “omega”Vincent Laporte
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-10-14ClassicalFacts.v: Unifying format for bibliographical references.Hugo Herbelin
2019-10-14Weak excluded-middle: adding a reference.Hugo Herbelin
2019-10-14Logic: Add equivalence between weak excluded-middle and classical Morgan's lawHugo Herbelin
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-16Define morphisms of real numbers and accelerate Cauchy realsVincent Semeria
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-09-10Merge PR #9406: [stdlib] Do not put INR_eq in the “real” hint databasePierre-Marie Pédrot
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-09-03Add lemmas directly relating List.nth and List.nth_errorOliver Nash
2019-09-03Remove redundant parameter in List.concat_filter_mapOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-09-01edits per reviewYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-29Merge PR #10703: Make Bool.eqb_spec transparentHugo Herbelin
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26Tauto: use Coqlib to locate “not” and “NNPP”Vincent Laporte
2019-08-25Make Bool.eqb_spec transparentTej Chajed
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-10Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else fa...Vincent Semeria
2019-08-09Switch constructive Rlt to sort Type, to make it compute laterVincent Semeria
2019-08-08Fix namespace of Cauchy realsVincent Semeria
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-06Prove the completeness of real numbers from logical axiom sig_not_decVincent Semeria
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 18:31:03 +0000