aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in th...Pierre-Marie Pédrot
2019-10-21Improvements of zifyFrédéric Besson
2019-10-21Adding changelogHugo Herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ...Gaëtan Gilbert
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and clas...Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
2019-10-14Updating changelogHugo Herbelin
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-11Document Gaëtan's new script to prefill a changelog entry.Théo Zimmermann
2019-10-09Fix alphabetical ordering in the list of contributors to 8.10.Théo Zimmermann
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to reduc...Vincent Laporte
2019-10-04Improve language.Théo Zimmermann
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint data...Pierre-Marie Pédrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:16:12 +0000