aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Expand)AuthorAge
* Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\
* \ Merge PR #1080: Remove some unused parts of the reference manual.Gravatar Maxime Dénès2017-10-03
|\ \
* | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| * | Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
* | | Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
|/ /
| * Reference manual: A few words about the file system constraints for -Q/-R.Gravatar Hugo Herbelin2017-09-13
|/
* Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\
* \ Merge PR #1035: Fix the introduction of SSR refman chapter.Gravatar Maxime Dénès2017-09-11
|\ \
* \ \ Merge PR #1014: Add option index entry for NativeCompute ProfilingGravatar Maxime Dénès2017-09-11
|\ \ \
* \ \ \ Merge PR #1004: Document primitive projections in more detailGravatar Maxime Dénès2017-09-11
|\ \ \ \
| | | | * Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
| |_|_|/ |/| | |
| | | * Fix the introduction of SSR refman chapter.Gravatar Théo Zimmermann2017-09-08
| |_|/ |/| |
* | | 2 Typos in 'Add Parametric Morphism' DocumentationGravatar staffehn2017-09-03
| | * add option index entry for NativeCompute ProfilingGravatar Paul Steckler2017-09-01
| |/ |/|
| * Document primitive projections in more detailGravatar Matthieu Sozeau2017-08-31
| * RefMan-ssr: fix warningGravatar Matthieu Sozeau2017-08-31
* | Merge PR #993: Credits for version 8.7Gravatar Maxime Dénès2017-08-31
|\ \
| * | Credits for version 8.7Gravatar Matthieu Sozeau2017-08-31
* | | Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \ | |_|/ |/| |
| * | coq_makefile: improve documentationGravatar Enrico Tassi2017-08-29
| |/
* | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\ \
* | | Fix obsolete description of real numerals.Gravatar Guillaume Melquiond2017-08-22
| |/ |/|
| * use OCaml temp_file, instead of our own versionGravatar Paul Steckler2017-08-18
* | Merge PR #973: Adding documentation for Printing Focused option.Gravatar Maxime Dénès2017-08-18
|\ \
| | * Add native compute profiling, BZ#5170Gravatar Paul Steckler2017-08-17
| |/ |/|
* | Merge PR #974: Change section caption, improve some wordingGravatar Maxime Dénès2017-08-17
|\ \
* | | Document anonymous universes (PR #544).Gravatar Gaëtan Gilbert2017-08-17
| | * Adding documentation for Printing Focused option.Gravatar Pierre Courtieu2017-08-17
| |/ |/|
| * mention that tactic is the identity or gives errorGravatar Paul Steckler2017-08-16
| * change section caption, improve some wordingGravatar Paul Steckler2017-08-16
|/
* Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleGravatar Maxime Dénès2017-08-16
|\
* \ Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #943: Reference Manual: minor wording improvementsGravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #934: Fix some coq-tex errors in the reference manual.Gravatar Maxime Dénès2017-08-16
|\ \ \ \
* \ \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \ \
| | | | | * Rewording the introductionGravatar Enrico Tassi2017-08-02
| | | | | * Rephrasing a couple of sentences in a more factual way.Gravatar Hugo Herbelin2017-08-02
| | | | | * Rephrasing the introduction in a more factual and up-to-date way.Gravatar Hugo Herbelin2017-08-02
| | | | | * Port ssr manual to Coq's latex/hevea styleGravatar Enrico Tassi2017-08-02
| |_|_|_|/ |/| | | |
| | | | * Update Setoid.texGravatar larsr2017-08-02
| |_|_|/ |/| | |
| * | | Typo in the documentation of cumulativityGravatar Amin Timany2017-08-02
* | | | Merge PR #933: Fix documentation of Hint Mode (bug #4911).Gravatar Maxime Dénès2017-08-01
|\ \ \ \
* \ \ \ \ Merge PR #932: Fix shuffled documentation.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR #929: Add missing paragraph to introductionGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #925: Document Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \
| | | | | | | | * Fix incorrect use of "At the end".Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | * Minor grammar fix: replace a "then" with a "so".Gravatar Sam Pablo Kuper2017-07-31
| |_|_|_|_|_|_|/ |/| | | | | | |
| | | | | | * | Update documentation of cumulativityGravatar Amin Timany2017-07-31
| | | | | | * | Fix typo and Add Jason's example to the docGravatar Amin Timany2017-07-31