aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-08-08[doc][ssr][under][setoid] Add changelog entryErik Martin-Dorel
2019-08-08[ssr] under: Add a contrived example to test under/over with SetoidsErik Martin-Dorel
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
2019-08-06[ssr] export Ssrequality.ssr_is_setoidErik Martin-Dorel
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive Projec...Théo Zimmermann
2019-08-05Merge PR #10608: Copy edit the Ltac2 documentationJim Fehrle
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-05Merge PR #10585: [coqdoc] Simplify regex for identifiers in commentsVincent Laporte
2019-08-05Merge PR #10445: Split constructive and classical axioms for real numbersVincent Laporte
2019-08-05ConstructiveCauchyReals: make explicit structural recursionVincent Laporte
2019-08-04Add missing file ide/default_bindings_src.exe to "make clean"Jim Fehrle
2019-08-04Merge PR #10579: Remove underscores from inserted texts.Pierre-Marie Pédrot
2019-08-02Merge PR #10543: Remove unused grammar nonterminals and productionsEnrico Tassi
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-08-02Merge PR #10553: Use a more traditional definition for uint63_div21 (fixes #1...Maxime Dénès
2019-07-31Merge PR #9811: [stdlib] Remove deprecated module ZlogarithmEmilio Jesus Gallego Arias
2019-07-30Merge PR #10594: Fix issue #10593 : Software foundations URL changedEmilio Jesus Gallego Arias
2019-07-30Merge PR #10595: [CI/Azure/macOS] Unshallow the homebrew-core repositoryEmilio Jesus Gallego Arias
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
2019-07-29Add a non-overflow precondition to diveucl_21 to align it on standard impleme...thery
2019-07-29Add test from #10551.Guillaume Melquiond
2019-07-29Transpose the C code of uint63_div21 to the OCaml implementations.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
2019-07-29[CI/Azure/macOS] Unshallow the homebrew-core repositoryVincent Laporte
2019-07-29Fix issue #10593 : Software foundations URL changedMichael Soegtrop
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
2019-07-29Merge PR #10581: Remove the tactic wizard, as it has not worked for several y...Pierre-Marie Pédrot
2019-07-29Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.Pierre-Marie Pédrot
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-07-27Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distrHugo Herbelin
2019-07-27[coqdoc] Simplify regex for identifiers in commentsLysxia
2019-07-26Remove unused grammar productionsJim Fehrle
2019-07-26Fix typoVincent Semeria
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one c...Guillaume Melquiond
2019-07-26Remove underscores from inserted texts.Guillaume Melquiond
2019-07-26Merge PR #10563: changed name of cos3PI4 to cos_3PI4 for consistencyMichael Soegtrop
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-07-26[stdlib] Remove deprecated module ZlogarithmVincent Laporte
2019-07-26Merge PR #10568: Mark primitive integers as able to participate in reductions...Maxime Dénès
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-25[Int63] Remove redundant misnamed lemma lsr_add_distrVincent Laporte
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-24changed name of cos3PI4 to cos_3PI4 for consistencyRobert Rand
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-24Merge PR #10549: [lemmas] Small cleanupsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 21:09:48 +0000