aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Merge PR #1116: Updating citing Coq in FAQ.Gravatar Maxime Dénès2017-10-10
|\
| * Updating citing Coq in FAQ.Gravatar Hugo Herbelin2017-10-10
| |
* | Fix copyright info in reference manual.Gravatar Théo Zimmermann2017-10-06
| | | | | | | | Also simplifies the way it is presented (no need to be overly precise).
* | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ \ | | | | | | | | | to escape non-UTF-8 file names)
* \ \ 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
| |_|/ |/| | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| * | 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
|\ \ \
* \ \ \ 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
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 18:08:55 +0000