aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add tests for primitive floats with 'vm_compute'Guillaume Bertholon
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-11-01Add tests for primitive floatsGuillaume Bertholon
2019-11-01Add Floats to standard libraryGuillaume Bertholon
2019-11-01Add primitive floats to Ltac2Pierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
2019-11-01[ssr] Update doc for under w.r.t. setoid-like relationsErik Martin-Dorel
2019-11-01[ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)Erik Martin-Dorel
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-31Merge PR #11021: Fix build in masterPierre-Marie Pédrot
2019-10-31lra: use “lia” rather than “omega”Vincent Laporte
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
2019-10-31Merge PR #10983: QArith, Lia: depend on ZArith_base rather than on ZArithPierre-Marie Pédrot
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
2019-10-31enforcing Ltac2 constructor name are uppercasedKenji Maillard
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-31Merge PR #11000: make: guard cp calls with rm -f on executablesPierre-Marie Pédrot
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ...Emilio Jesus Gallego Arias
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-31restore red behaviour printingGaëtan Gilbert
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Doc: index command Arguments with assertGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
2019-10-31[classes] Remove a couple of unneeded option typesEmilio Jesus Gallego Arias
2019-10-31[classes] Untabify in preparation for next commit.Emilio Jesus Gallego Arias
2019-10-31[classes] Some refactoring on proof save preparation.Emilio Jesus Gallego Arias
2019-10-31Merge PR #11009: Rename the 2 local type_cstr nonterminals to give them uniqu...Pierre-Marie Pédrot
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
2019-10-31[Nix] Update reference to nixpkgsVincent Laporte
2019-10-30Merge PR #10953: [declare] Remove declare_scheme hook in DeclarePierre-Marie Pédrot
2019-10-30Merge PR #11004: [test-suite] Test section-local mutual Fixpoint.Pierre-Marie Pédrot
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Merge PR #10999: [refman] Give an example of contradiction when positivity ch...Clément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 02:16:38 +0000