aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Merge PR #9384: Improve the note in the beginning of the Ltac chapter.Clément Pit-Claudel
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-24Merge PR #9392: Fix small errors in cic.rst.Théo Zimmermann
2019-01-24use \nO, \nS, etc. fix \kw{n}.Tanaka Akira
2019-01-24Fix small errors in cic.rst.Tanaka Akira
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
2019-01-23Fix the information of the level of ; vs ; [ ]Théo Zimmermann
2019-01-23Improve the note in the beginning of the Ltac chapter.Théo Zimmermann
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2019-01-21ring and field simplify can take no argumentsthery
2019-01-21Merge PR #9304: Default disable auto template warning.Maxime Dénès
2019-01-11Merge pull request #8778 from SkySkimmer/merge-plugin-tutoYves Bertot
2019-01-09[Manual] Remove link to non-existing CSS fileVincent Laporte
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2019-01-08plugin_tutorial: ignore Coqlib.find_reference deprecation warning.Gaëtan Gilbert
2019-01-08Add 'doc/plugin_tutorial/' from commit '168a13dab1c9987f592994150997e692d4d7e...Gaëtan Gilbert
2019-01-08Add doc for auto-template warningGaëtan Gilbert
2018-12-26[dune] Build refman with fatal warnings by default like in the Makefile build.Théo Zimmermann
2018-12-21Merge PR #9247: Fix typo in gallina specification language docThéo Zimmermann
2018-12-19[doc] typoEnrico Tassi
2018-12-19Fix typo in gallina specification language docyudetamago
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-12-14Merge PR #9073: [sphinx] No more undocumented objects.Clément Pit-Claudel
2018-12-14Merge PR #9147: [dune] [doc] Support for building the reference manual with D...Théo Zimmermann
2018-12-14Turn warning on for undocumented objects. Closes #7602.Théo Zimmermann
2018-12-14Fix the SSReflect chapter regarding objects without bodies.Théo Zimmermann
2018-12-14Do not raise object without body warning for prodn objects.Théo Zimmermann
2018-12-13Merge PR #9211: Fixing incorrect mention of coercions as being part of the in...Théo Zimmermann
2018-12-13[dune] [doc] Support for building the reference manual with Dune.Emilio Jesus Gallego Arias
2018-12-13Merge PR #9196: Document the deprecation of hint declaration withou database ...Maxime Dénès
2018-12-12Fixing incorrect mention of coercions as being part of the interning phase.Hugo Herbelin
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-11Add missing formatting.Théo Zimmermann
2018-12-11Document the deprecation of hint declaration withou database in refman.Théo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
2018-12-03[sphinx] Same rendering for :n:`@token` and :token:`token`.Théo Zimmermann
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-30Merge PR #9105: Add indexes for coercion / substructure symbol :>.Clément Pit-Claudel
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-28Fix numeral notations doc by indentingJason Gross
2018-11-28Fix string notation docJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:22:36 +0000