| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-11 | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | |
| 2017-09-11 | Merge PR #1035: Fix the introduction of SSR refman chapter. | Maxime Dénès | |
| 2017-09-11 | Merge PR #1014: Add option index entry for NativeCompute Profiling | Maxime Dénès | |
| 2017-09-11 | Merge PR #1004: Document primitive projections in more detail | Maxime Dénès | |
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-09-08 | Fix the introduction of SSR refman chapter. | Théo Zimmermann | |
| 2017-09-03 | 2 Typos in 'Add Parametric Morphism' Documentation | staffehn | |
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler | |
| 2017-09-01 | Fixing various typos in the Credits chapter. | Théo Zimmermann | |
| 2017-08-31 | Document primitive projections in more detail | Matthieu Sozeau | |
| 2017-08-31 | RefMan-ssr: fix warning | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #993: Credits for version 8.7 | Maxime Dénès | |
| 2017-08-31 | Credits for version 8.7 | Matthieu Sozeau | |
| 2017-08-31 | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | |
| 2017-08-29 | coq_makefile: improve documentation | Enrico Tassi | |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-29 | Merge PR #988: Fix obsolete description of real numerals. | Maxime Dénès | |
| 2017-08-29 | Merge PR #819: Cleanup old things | Maxime Dénès | |
| 2017-08-29 | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | |
| 2017-08-23 | Update coypright dates on documentation | Matthieu Sozeau | |
| 2017-08-22 | Fix obsolete description of real numerals. | Guillaume Melquiond | |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler | |
| 2017-08-18 | Merge PR #973: Adding documentation for Printing Focused option. | Maxime Dénès | |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-17 | Merge PR #974: Change section caption, improve some wording | Maxime Dénès | |
| 2017-08-17 | Document anonymous universes (PR #544). | Gaëtan Gilbert | |
| 2017-08-17 | Adding documentation for Printing Focused option. | Pierre Courtieu | |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 2017-08-16 | Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style | Maxime Dénès | |
| 2017-08-16 | Merge PR #948: [doc] Write (@nil nat) instead of (nil nat) | Maxime Dénès | |
| 2017-08-16 | Merge PR #943: Reference Manual: minor wording improvements | Maxime Dénès | |
| 2017-08-16 | Merge PR #940: Replace jarring use of "Remark" with "Note" | Maxime Dénès | |
| 2017-08-16 | Merge PR #934: Fix some coq-tex errors in the reference manual. | Maxime Dénès | |
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-02 | Rewording the introduction | Enrico Tassi | |
| 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. | |||
| 2017-08-02 | Rephrasing a couple of sentences in a more factual way. | Hugo Herbelin | |
| 2017-08-02 | Rephrasing the introduction in a more factual and up-to-date way. | Hugo Herbelin | |
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | |
| Work done by Assia Mahboubi and Enrico Tassi | |||
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi | |
| 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). | |||
| 2017-08-02 | Update Setoid.tex | larsr | |
| The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | |||
| 2017-08-02 | Typo in the documentation of cumulativity | Amin Timany | |
| 2017-08-01 | Unbreak RecTutorial.v | Gaëtan Gilbert | |
| The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it. | |||
| 2017-08-01 | Remove old doc/rt files. | Gaëtan Gilbert | |
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-08-01 | Improve style slightly | Sam Pablo Kuper | |
| per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940). | |||
| 2017-08-01 | Merge PR #933: Fix documentation of Hint Mode (bug #4911). | Maxime Dénès | |
| 2017-08-01 | Merge PR #932: Fix shuffled documentation. | Maxime Dénès | |
| 2017-08-01 | Merge PR #929: Add missing paragraph to introduction | Maxime Dénès | |
| 2017-08-01 | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |