aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2019-10-22documentation fixesAntonio Nikishaev
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.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-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
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-09Fix alphabetical ordering in the list of contributors to 8.10.Théo Zimmermann
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-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-03Improved handling of micromega cachesFrédéric Besson
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
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-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-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
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-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-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
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-05Merge PR #10624: Remove reference to removed option Printing Primitive Projec...Théo Zimmermann
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
2019-07-29Document changes by PR 10324Vincent Laporte
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one c...Guillaume Melquiond
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès