aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Move extended pattern matching to new location.Théo Zimmermann
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
2020-04-27Further documentation improvements.Théo Zimmermann
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-22Document `+` in polymorphic universe levelsKenji Maillard
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-12Update doc/sphinx/addendum/extended-pattern-matching.rstlarsr
2020-03-12Fixed link to "match" syntax. larsr
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-08Add documentation for extraction of ascii and string literalsMaxime Dénès
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...Théo Zimmermann
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-27weaker then -> weaker thanlarsr
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
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-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
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-01-31 11:40:27 +0000