aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* 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
|\ \ \
* \ \ \ Merge PR #988: Fix obsolete description of real numerals.Gravatar Maxime Dénès2017-08-29
|\ \ \ \
* \ \ \ \ Merge PR #819: Cleanup old thingsGravatar Maxime Dénès2017-08-29
|\ \ \ \ \
* \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | | | | * Update coypright dates on documentationGravatar Matthieu Sozeau2017-08-23
| |_|_|_|/ |/| | | |
| | | * | 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 #940: Replace jarring use of "Remark" with "Note"Gravatar 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The contents should be exactly the same. I removed the distinction between tactical and pseudo-tactical because I think that it is too much technical for the introduction. I used "syntactic construction" and made appeal to the reader intuition by saying that such construction behaves similarly to a tactical. I think the text would be much more readable if "the tactics described in Chapter..." could be replaced by a *name*, but I'm afraid the only one I could use (Ltac) is a bit too ambiguous. So I'm open to suggestions.
| | | | | | * | | 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
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Work done by Assia Mahboubi and Enrico Tassi
| | | | | | * | | Makefile.doc: implement serve-refman-8080 targetGravatar Enrico Tassi2017-08-02
| |_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python).
| | | | | * | | Update Setoid.texGravatar larsr2017-08-02
| |_|_|_|/ / / |/| | | | | | | | | | | | | The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`.
| * | | | | | Typo in the documentation of cumulativityGravatar Amin Timany2017-08-02
| | | | | | |
| | | | | | * Unbreak RecTutorial.vGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it.
| | | | | | * Remove old doc/rt files.Gravatar Gaëtan Gilbert2017-08-01
| |_|_|_|_|/ |/| | | | |
| | | | | * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
| | | * | Improve style slightlyGravatar Sam Pablo Kuper2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
* | | | | 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
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 20:18:59 +0000