| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-15 | [Sphinx] Move chapter 13 to new infrastructure | Maxime Dénès | |
| 2018-03-04 | [compat] Remove NOOP and alias deprecated options. | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP. | |||
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert | |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert | |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-07-28 | Fix some coq-tex errors in the reference manual. | Guillaume Melquiond | |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | |
| The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | |||
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot | |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2014-10-03 | Fixing #3606 continued (doc of Scheme Boolean Equality Scheme). | Hugo Herbelin | |
| 2014-09-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵ | Arnaud Spiwack | |
| Schemes] option. | |||
| 2014-07-01 | Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes" | Hugo Herbelin | |
| 2012-09-15 | Port rewrites of tactic documentation from branch 8.4. | gmelquio | |
| This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277, r15278, r15337. The merge did not go without troubles, but hopefully none of the changes were lost in process. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |