aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Collapse)AuthorAge
* Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
|
* [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.
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
|
* Silence some warning about references in documentation.Gravatar Guillaume Melquiond2013-12-03
|
* First stab at documenting Canonical StructuresGravatar Enrico Tassi2013-11-29
|
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of the "Local Definition" command.Gravatar ppedrot2013-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
| | | | | | | Also started a preliminary documentation about evars (where to have it in the doc is somehow open). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16234 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving rendering of ...-separated lists and sequences in referenceGravatar herbelin2012-08-11
| | | | | | | manual (making style uniform: no {\tt \ldots}; using only one space when there is no delimiters in the sequence). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of records defined with the keywords Inductive andGravatar aspiwack2012-04-13
| | | | | | CoInductive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added documentation for "Set Parsing Explicit" + fixed mistakenlyGravatar herbelin2012-01-20
| | | | | | committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
| | | | | | | | | arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of Arguments + implicitsGravatar gareuselesinge2011-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
| | | | | | | | | | | that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
| | | | | | | | when printing. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14284 85f007b7-540e-0410-9357-904b9bb8a0f7
* @ in index of refman (last request of bug 2494)Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)Gravatar herbelin2011-04-06
| | | | | | (backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix formatting issue in refmanGravatar glondu2011-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document DOT output of universe graphGravatar glondu2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13612 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 15:02:11 +0000