aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Expand)Author
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
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
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
2019-11-03Elan → Stratego in documentation of `rewrite_strat`.Robbert Krebbers
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
2019-10-14Merge PR #10811: Allow SProp default onPierre-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-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-16Re-implementation of zifyFrédéric Besson
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert