| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-15 | [Sphinx] Move chapter 2 to new infrastructure | Maxime Dénès | |
| 2017-12-12 | Documenting the new options for printing "match". | Hugo Herbelin | |
| Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause. | |||
| 2017-10-24 | Fix part of 'Hard to find documentation for `(...) and `{...} #5631' | Johannes Kloos | |
| As discussed in the bug report, this adds `(...) and `{...} to the index. | |||
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-09-11 | Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit` | Maxime Dénès | |
| 2017-09-08 | Fix Typo in Doc for `Set Parsing Explicit` | staffehn | |
| 2017-08-31 | Document primitive projections in more detail | Matthieu Sozeau | |
| 2017-07-14 | Update with non structurally recursive | william-lawvere | |
| 2017-07-07 | RefMan-ext: fix some typos | William Lawvere | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-23 | Merge PR#740: Refactor documentation of records. | Maxime Dénès | |
| 2017-06-16 | Refactor documentation of records. | Théo Zimmermann | |
| This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971 | |||
| 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. | |||
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann | |
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-09 | Merge PR#460: Turning the printing primitive projection compatibility flag ↵ | Maxime Dénès | |
| off by default | |||
| 2017-04-07 | Merge PR#485: Document Show Match | Maxime Dénès | |
| 2017-04-07 | Turning the printing primitive projection parameter flag off by default. | Hugo Herbelin | |
| 2017-04-07 | Turning the printing primitive projection compatibility flag off by default. | Hugo Herbelin | |
| 2017-03-23 | Documenting the grammar {| ... |} syntax for building records. | Hugo Herbelin | |
| And an extra minor changes (use of zeroone when relevant, use of type rather than term). | |||
| 2017-03-17 | Document Show Match, add ref to that in match variants/extensions | Paul Steckler | |
| 2017-03-14 | [toplevel] Remove unusable option -notop | Emilio Jesus Gallego Arias | |
| Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 . | |||
| 2016-11-08 | Update documentation of Arguments after recent changes. | Maxime Dénès | |
| 2016-01-20 | Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. | Maxime Dénès | |
| 2015-12-12 | Indexing and documenting some options. | Pierre-Marie Pédrot | |
| 2015-12-10 | RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions". | Hugo Herbelin | |
| 2015-12-06 | RefMan, ch. 1 and 2: avoiding using the name "constant" when | Hugo Herbelin | |
| "constructor" and "inductive" are meant also. | |||
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-26 | Adding the Printing Projections options to the index. | Pierre-Marie Pédrot | |
| 2015-07-30 | Fix some broken Coq scripts in the documentation. | Guillaume Melquiond | |
| 2015-07-22 | Remove obsolete documentation. (Fix bug #4238) | Guillaume Melquiond | |
| 2015-04-01 | Fixing a few typos + some uniformization of writing in doc. | Hugo Herbelin | |
| 2015-04-01 | More clarifications on loadpaths. | Pierre-Marie Pédrot | |
| 2015-04-01 | Documenting "From * Require *" and clearing a bit the loadpath chapter. | Pierre-Marie Pédrot | |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | |
| 2015-02-12 | Make clearer that "Remove Printing Let" does not influence destructuring let. | Guillaume Melquiond | |
| 2015-02-10 | Prevent Latex from messing with backticks. (Fix for bug #3871) | Guillaume Melquiond | |
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond | |
| 2015-01-29 | Remove some "Warning:" from the reference manual. | Guillaume Melquiond | |
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin | |
| Set Printing Existential Instances (see bug report #3951). | |||
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau | |
| 2014-12-09 | refman: switch all source files to utf8 | Pierre Letouzey | |
| Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources. | |||
| 2014-10-22 | Move 'Arguments: clear implicits' to 2.7.4 (Close 2891) | Enrico Tassi | |
| 2014-09-29 | typo | Enrico Tassi | |
| 2014-09-18 | seems to fix a looping coq-tex (when compiled with camlp4) | Pierre Boutillier | |
| 2014-09-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵ | Arnaud Spiwack | |
| Schemes] option. | |||
| 2014-09-03 | sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex | Pierre Boutillier | |
| 2014-09-03 | Update RefMan with respect to new loadpath management | Pierre Boutillier | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |