aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add Floats to standard libraryGuillaume Bertholon
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
2019-10-31Merge PR #10994: Numbers.Cyclic: use “lia” rather than “omega”Pierre-Marie Pédrot
2019-10-31Merge PR #10937: [stdlib]Reals: use “lia” rather than “omega”Pierre-Marie Pédrot
2019-10-31lia: depend only on ZArith_baseVincent Laporte
2019-10-31QArith: only depend on ZArith_baseVincent Laporte
2019-10-31Zdigits: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zquot: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zpow_facts: use “lia” rather than “omega”Vincent Laporte
2019-10-31Zwf: use “lia” rather than “omega”Vincent Laporte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:26:32 +0000