aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2017-08-16change section caption, improve some wordingPaul Steckler
2017-08-16Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleMaxime Dénès
2017-08-16Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Maxime Dénès
2017-08-16Merge PR #943: Reference Manual: minor wording improvementsMaxime Dénès
2017-08-16Merge PR #940: Replace jarring use of "Remark" with "Note"Maxime Dénès
2017-08-16Merge PR #934: Fix some coq-tex errors in the reference manual.Maxime Dénès
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-02Rewording the introductionEnrico Tassi
2017-08-02Rephrasing a couple of sentences in a more factual way.Hugo Herbelin
2017-08-02Rephrasing the introduction in a more factual and up-to-date way.Hugo Herbelin
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
2017-08-02Update Setoid.texlarsr
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-01Unbreak RecTutorial.vGaëtan Gilbert
2017-08-01Remove old doc/rt files.Gaëtan Gilbert
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Improve style slightlySam Pablo Kuper
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Fix incorrect use of "At the end".Sam Pablo Kuper
2017-07-31Minor grammar fix: replace a "then" with a "so".Sam Pablo Kuper
2017-07-31Replace jarring use of "Remark" with "Note"Sam Pablo Kuper
2017-07-31Update documentation of cumulativityAmin Timany
2017-07-31Fix typo and Add Jason's example to the docAmin Timany
2017-07-31Improve documentation of cumulativityAmin Timany
2017-07-29Drop paragraph mentioning Addendum as separate doc.Théo Zimmermann
2017-07-28Merge PR #823: Async off in Windows by default in CoqIDEMaxime Dénès
2017-07-28Fix some coq-tex errors in the reference manual.Guillaume Melquiond
2017-07-28Fix documentation of Hint Mode (bug #4911).Guillaume Melquiond
2017-07-28Fix shuffled documentation.Guillaume Melquiond
2017-07-27Add missing paragraph to introductionBenjamin Pierce
2017-07-27Extraction.tex: mention the possible "From Coq Require Extraction"letouzey
2017-07-27Extraction TestCompile documented + mentionned in CHANGESPierre Letouzey
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-19Merge PR #745: Add timing scriptsMaxime Dénès
2017-07-17Merge PR #865: RefMan-ext: fix some typosMaxime Dénès
2017-07-14Update with non structurally recursivewilliam-lawvere
2017-07-11Sync the manual with the deprecation warnings.Théo Zimmermann
2017-07-11Document the timing targetsJason Gross
2017-07-11Strip trailing spacesJason Gross
2017-07-07RefMan-ext: fix some typosWilliam Lawvere
2017-07-07Merge PR #842: Update the Tutorial.Maxime Dénès
2017-07-07Merge PR #835: Remove doc/refman/RefMan-ind.texMaxime Dénès
2017-07-05Merge PR #837: Add inversion_sigma to CHANGES and to docMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 15:37:53 +0000