aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ext.tex
AgeCommit message (Collapse)Author
2015-12-10RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Hugo Herbelin
2015-12-06RefMan, ch. 1 and 2: avoiding using the name "constant" whenHugo Herbelin
"constructor" and "inductive" are meant also.
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-26Adding the Printing Projections options to the index.Pierre-Marie Pédrot
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2015-07-22Remove obsolete documentation. (Fix bug #4238)Guillaume Melquiond
2015-04-01Fixing a few typos + some uniformization of writing in doc.Hugo Herbelin
2015-04-01More clarifications on loadpaths.Pierre-Marie Pédrot
2015-04-01Documenting "From * Require *" and clearing a bit the loadpath chapter.Pierre-Marie Pédrot
2015-02-17Separate index for vernacular options.Maxime Dénès
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-29Remove some "Warning:" from the reference manual.Guillaume Melquiond
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
Set Printing Existential Instances (see bug report #3951).
2015-01-15Move explanations about primitive projections to the manual.Matthieu Sozeau
2014-12-09refman: switch all source files to utf8Pierre 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-22Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)Enrico Tassi
2014-09-29typoEnrico Tassi
2014-09-18seems to fix a looping coq-tex (when compiled with camlp4)Pierre Boutillier
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵Arnaud Spiwack
Schemes] option.
2014-09-03sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texPierre Boutillier
2014-09-03Update RefMan with respect to new loadpath managementPierre Boutillier
2014-08-25"allows to", like "allowing to", is improperJason 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).
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual.
2013-12-11Documenting the tactic-in-term construction.Pierre-Marie Pédrot
2013-12-03Silence some warning about references in documentation.Guillaume Melquiond
2013-11-29First stab at documenting Canonical StructuresEnrico Tassi
2013-08-08Manual fixed w.r.t. STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Documentation of the "Local Definition" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-21Added missing documentation of Set Printing Existential Instances.herbelin
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
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin
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
2012-04-13Documentation of records defined with the keywords Inductive andaspiwack
CoInductive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
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
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Documentation of Arguments + implicitsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
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
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
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
2011-04-08@ in index of refman (last request of bug 2494)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13977 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-06Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)herbelin
(backport from 8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13961 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-12Fix formatting issue in refmanglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13791 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-01-11Add "Print Sorted Universes"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-11-02Document DOT output of universe graphglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13612 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Added multiple implicit arguments rules per name.herbelin
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
Updated documentation in many ways: - merged binder and binderlet as done for a while in implementation - fixed a few technical problems (bad indexation of {x:A|P x}, missing spaces in html code in many situations due to missing curly brackets around TeX macros - e.g. around \ldots -, missing dots at end of sentences, ...) - renamed "statement" commands into "assertion" commands and "declaration" commands into "assumption" commands - moved Goal and Save out of the Gallina chapter - avoid some recovering in the Gallina and proof mode chapters - slight smoothing of some hard-to-read paragraphs of the manual git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-06Correction in Function documentationjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12995 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
syntax of "Implicit Type" (that can now be "Implicit Types" and can now accept several blocks of variables of a given type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12960 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Document Generalizable Variables, and change syntax to msozeau
[Generalizable (All|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 01:47:41 +0000