aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Improved handling of micromega cachesFrédéric Besson
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-09-26Merge PR #10664: Putting sections libstack inside the kernelMaxime Dénès
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Fix syntax of reduction tactics when listing qualid to reduce or not.Théo Zimmermann
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-17Add changelog entryMaxime Dénès
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-16Re-implementation of zifyFrédéric Besson
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-09Merge PR #9379: Vectors: lemmas about uncons and splitAtHugo Herbelin
2019-09-05Merge PR #10731: Ocfnash/stdlib additionsHugo Herbelin
2019-09-05Merge PR #10730: Add missing index for From ... Require ...Clément Pit-Claudel
2019-09-04Add changelog entry for 10731Oliver Nash
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-09-03Apply suggestions from code reviewOliver Nash
2019-09-03New lemmas for List.vOliver Nash
2019-09-01edits per reviewYishuai Li
2019-09-01Changelog: more accurate on unconsYishuai Li
2019-09-01Vectors: lemmas about uncons and splitAtYishuai Li
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-25Merge PR #10632: Prove the completeness of real numbers from logical axiom si...Hugo Herbelin
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
2019-08-19Split ConstructiveRealsLUB and improve commentsVincent Semeria
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-09Add a changelog entryKazuhiko Sakaguchi
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-08[doc][ssr][under][setoid] Add changelog entryErik 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 08:04:48 +0000