aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-26Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ...coqbot-app[bot]
2020-08-25Documentation of coq_makefile: fix name of installation dir + help on option -f.Hugo Herbelin
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
2020-08-17Merge PR #12802: Document semantic restriction on patterns in Gallina match c...coqbot
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environm...coqbot
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-17Wording improvements.Théo Zimmermann
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
2020-06-21Add index for coqdoc.Théo Zimmermann
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
2020-06-14Update zify documentationFrédéric Besson
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 10:25:33 +0000