aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
2020-09-08[Small typo] Update match.rstClément Blaudeau
2020-09-08Merge PR #12927: Explain that tactics applied to multiple goals don't preserv...coqbot-app[bot]
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-09-07Add changelog entryEdward Wang
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-27[zarith] ChangelogEmilio Jesus Gallego Arias
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
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-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-19Improve `make approve-output`Jason Gross
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
2020-08-18Fix subject reduction VS cumulative inductives and function etaGaëtan Gilbert
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 #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
2020-08-13Merge PR #12479: Bring Int63 notations into line with stdlibAnton Trunov
2020-08-12Additional statements about List.repeatOlivier Laurent
2020-08-11add deprecation to changelogYishuai Li
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 Int63 notations into line with stdlibJason Gross
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environm...coqbot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:28:01 +0000