aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...Théo Zimmermann
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple producti...Théo Zimmermann
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-27docs: Update changes.rst w.r.t. ssrsetoid.v's simplificationErik Martin-Dorel
2019-12-25Show doc notations in boldfaceJim Fehrle
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
2019-12-22Apply suggestions from code reviewThéo Zimmermann
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-14Make prodn look more like productionlistJim Fehrle
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02List of 8.11 contributors and stats.Théo Zimmermann
2019-12-02Merge redundant consecutive changelog entries on reals.Théo Zimmermann
2019-12-02Highlight refine attribute for Instance.Théo Zimmermann
2019-12-02Warn more clearly about incompatibilities coming from #10476.Théo Zimmermann
2019-12-028.11 release notes.Matthieu Sozeau
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
2019-11-14doc fixesAntonio Nikishaev
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 07:40:15 +0000