aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Collapse)AuthorAge
* Documenting the new options for printing "match".Gravatar Hugo Herbelin2017-12-12
| | | | | | Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause.
* Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Gravatar Johannes Kloos2017-10-24
| | | | | As discussed in the bug report, this adds `(...) and `{...} to the index.
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
|
* Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Gravatar Maxime Dénès2017-09-11
|\
| * Fix Typo in Doc for `Set Parsing Explicit`Gravatar staffehn2017-09-08
| |
* | Document primitive projections in more detailGravatar Matthieu Sozeau2017-08-31
|/
* Update with non structurally recursiveGravatar william-lawvere2017-07-14
|
* RefMan-ext: fix some typosGravatar William Lawvere2017-07-07
|
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Merge PR#740: Refactor documentation of records.Gravatar Maxime Dénès2017-06-23
| |\
| | * Refactor documentation of records.Gravatar Théo Zimmermann2017-06-16
| | | | | | | | | | | | This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
* | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Document evar naming syntax.Gravatar Théo Zimmermann2017-06-13
| |/
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ | | | | | | | | | record fields.
* \ \ Merge PR#460: Turning the printing primitive projection compatibility flag ↵Gravatar Maxime Dénès2017-04-09
|\ \ \ | | | | | | | | | | | | off by default
* \ \ \ Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \ \
| | * | | Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | | | |
| | * | | Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |/ / / |/| | |
| | * | Documenting the grammar {| ... |} syntax for building records.Gravatar Hugo Herbelin2017-03-23
| |/ / |/| | | | | | | | | | | And an extra minor changes (use of zeroone when relevant, use of type rather than term).
| * | Document Show Match, add ref to that in match variants/extensionsGravatar Paul Steckler2017-03-17
| |/
* / [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
|/ | | | | | | | | | | | | | | | | | | | | | | 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 .
* Update documentation of Arguments after recent changes.Gravatar Maxime Dénès2016-11-08
|
* Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
|
* Indexing and documenting some options.Gravatar Pierre-Marie Pédrot2015-12-12
|
* RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Gravatar Hugo Herbelin2015-12-10
|
* RefMan, ch. 1 and 2: avoiding using the name "constant" whenGravatar Hugo Herbelin2015-12-06
| | | | "constructor" and "inductive" are meant also.
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
|
* Adding the Printing Projections options to the index.Gravatar Pierre-Marie Pédrot2015-11-26
|
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
|
* Remove obsolete documentation. (Fix bug #4238)Gravatar Guillaume Melquiond2015-07-22
|
* Fixing a few typos + some uniformization of writing in doc.Gravatar Hugo Herbelin2015-04-01
|
* More clarifications on loadpaths.Gravatar Pierre-Marie Pédrot2015-04-01
|
* Documenting "From * Require *" and clearing a bit the loadpath chapter.Gravatar Pierre-Marie Pédrot2015-04-01
|
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
|
* Make clearer that "Remove Printing Let" does not influence destructuring let.Gravatar Guillaume Melquiond2015-02-12
|
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
|
* Fix index of reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
|
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
| | | | Set Printing Existential Instances (see bug report #3951).
* Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-15
|
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
| | | | | | 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.
* Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Gravatar Enrico Tassi2014-10-22
|
* typoGravatar Enrico Tassi2014-09-29
|
* seems to fix a looping coq-tex (when compiled with camlp4)Gravatar Pierre Boutillier2014-09-18
|
* Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵Gravatar Arnaud Spiwack2014-09-04
| | | | Schemes] option.
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
|
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | 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).
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
| | | | | Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 21:00:18 +0000