aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-25PermutEq: use “lia” rather than “omega”Vincent Laporte
2019-11-25PermutSetoid: use “lia” rather than “omega”Vincent Laporte
2019-11-25MSets: use “lia” rather than “omega”Vincent Laporte
2019-11-13Register proof_irrelevancePierre Roux
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:54:23 +0000