aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ext.tex
Commit message (Collapse)AuthorAge
* 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
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
| | | | | | | | | 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
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
| | | | | | | | | | | | | | | | 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
* Correction in Function documentationGravatar jforest2010-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
| | | | | | | 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
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
| | | | | | | | | [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
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
| | | | | | | | | | - Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Last changes in type class syntax: Gravatar msozeau2009-01-18
| | | | | | | | | | | | - curly braces mandatory for record class instances - no mention of the unique method for definitional class instances Turning a record or definition into a class is mostly a matter of changing the keywords to 'Class' and 'Instance' now. Documentation reflects these changes, and was checked once more along with setoid_rewrite's and Program's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
| | | | | | | | | late 2008 Coq WG. - Updated Copyright file wrt JProver. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
| | | | | | | | | | | | | | | | | - Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
| | | | | | | | | | "set (f:=fun n => t)" (et idem pour pose). Documentation notation Record sans sort et, en passant, "let|" -> "let '". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10852 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix examples in Program documentation and add comindexes for the variousGravatar msozeau2008-03-23
| | | | | | | | commands. Update documentation of implicit arguments with the new syntax and an explanation for the way it works in inductive type definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
| | | | | | | | | only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of CHANGES and refman doc for the implicit argument binderGravatar msozeau2008-02-08
| | | | | | | `X`. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10538 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation des nouvelles options d'implicites (Set Strongly StrictGravatar herbelin2008-02-06
| | | | | | | | | | | Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with |- ?A -> ?B => intro | _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish let| implementation and document itGravatar msozeau2008-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation du format des références croisées vers Figure, Section, ↵Gravatar herbelin2008-01-05
| | | | | | | | | | | Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
| | | | | | | | | | Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some typos.Gravatar glondu2007-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed many refman/*.tex files. Put \label and \index commands that ↵Gravatar emakarov2007-04-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | immediately follow sectioning commands insides those sectioning commands. If \label{...} is placed after \section{...}, then, when clicking on the link in the HTML file produced by Hevea, we are moved to the correct section, but the section header is just above the screen. Hevea manual recommends writing \section{...\label{...}} and similarly for index. On the other hand, writing commands inside the argument of sectioning commands is potentially dangerous because these arguments are reproduced not only to produce the section header but also to produce headers and/or table of contents entries. Thus, \index{...} and \labels{...} may be executed several times. Indeed, if we put a \typeout{...} instruction inside the argument to a sectioning command then it will be executed, besides the section itself, in the table of contents and once for every appearance of the header. However, it seems that the \label command are not executed several times unless they are prefixed with \protect, and \index command is not executed multiple times even then. So maybe it's OK to put \label and \index inside sectioning commands. When hyperref package is used, the \newlabel command left in .aux file has an extra group {...} which includes another \label command! This may lead to trouble when we use \nameref (?). However, the most reliable way would be to use the optional argument of sectioning commands. Then the text only goes to the optional argument and the text plus \label plus \index goes to the main argument. The optional argument is used for headers and table of contents. This works fine with Hevea as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned doc/common/title.tex file. Increased the space under headersGravatar emakarov2007-04-12
| | | | | | | in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleur anglais (cf 9619)Gravatar herbelin2007-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relecture/nettoyage chapitre Gallina; déplacement section FunctionGravatar herbelin2007-02-07
| | | | | | | | | dans extensions de Gallina. Divers. (report revisions 9614 et 9594 de la branche 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9615 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 11:22:16 +0000