aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common
Commit message (Collapse)AuthorAge
* 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).
* Fix broken documentation in presence of \zeroone{... \tt ...}.Gravatar Guillaume Melquiond2016-12-06
| | | | | | | | | | | | | The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
* Update copyright on documentation cover.Gravatar Maxime Dénès2016-11-30
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\
| * FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
|/ | | | In particular, documenting bracketing of last pattern on by default.
* ENH: examples for 'strict positivity' were expandedGravatar Matej Kosik2015-12-10
|
* CLEANUP: s/List_A/List~A/gGravatar Matej Kosik2015-12-10
|
* CLEANUP: superfluous examples were removedGravatar Matej Kosik2015-12-10
|
* ENH: new example: "even"Gravatar Matej Kosik2015-12-10
|
* ALPHA-CONVERSION: s/Length/has_length/gGravatar Matej Kosik2015-12-10
|
* ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ↵Gravatar Matej Kosik2015-12-10
| | | | | | order to make it more concrete and more comprehensible. This ver
* RefMan, ch. 4: Removing the local context of inductive definitions.Gravatar Hugo Herbelin2015-12-10
|
* RefMan, ch. 4: Adding discharging of inductive types.Gravatar Hugo Herbelin2015-12-10
|
* RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a localGravatar Hugo Herbelin2015-12-10
| | | | | | | | | | context for discharge in global declarations. Discharge now done on a global declaration. Hence removed Def and Assum which were only partially used (e.g. in rules Def and Assum but not in delta-conversion, nor in rule Const). Added discharge rule over definitions using let-in. It replaces the "substitution" rule since about 7.0.
* RefMan, ch. 4: Reformulating introduction of the chapter on CIC, beingGravatar Hugo Herbelin2015-12-10
| | | | | | | | | | clearer that the version depends on the version of Coq. Also renouncing to the "Predicative" and "(Co)" in the name, since after all, usage seems to continue calling the language of Coq Calculus of Inductive Constructions and to consider the Set predicative vs Set impredicative, as well as the presence of coinduction, as flavors of the CIC.
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Refresh some copyright headers.Gravatar Maxime Dénès2015-01-13
|
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
| | | | Updated doc, but not tests-suite yet.
* 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.
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
| | | | | | | | | | | Unfortunately, these ?uri=referer parameters do not work correctly now that coq.inria.fr forces the switch to https before answering any document. See: http://validator.w3.org/docs/help.html#faq-referer I currently see no workaround for that, apart from generating links like ?uri=http://the.real.url/of/my/page, which would be quite painful. For now, users interested in checking the validity of our pages will have to copy-paste the url they want to check after clicking on the validator button.
* refman: xhtml validity of the cover pageGravatar Pierre Letouzey2014-12-09
|
* doc: improved xhtml compatibility (cover, header,...)Gravatar Pierre Letouzey2014-12-09
|
* doc/stdlib: fix the html charset in header.html and coGravatar Pierre Letouzey2014-12-09
|
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-12-09
| | | | To be continued someday, those style files are full of redundancies...
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵Gravatar notin2014-12-09
| | | | documentation en ligne)
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵Gravatar notin2014-12-09
| | | | | | documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
|
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
|
* Beautify tactic documentation a bit more.Gravatar gmelquio2012-09-16
| | | | | | | | - Do not use \\ in place of empty lines. - Fix missing spaces after some \dots. - Do not use monospace slanted for clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove superfluous spaces and commas in tactic documentation.Gravatar gmelquio2012-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
| | | | | | much of them). Improving doc of conversion clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 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
* Documenting eta-conversion.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15708 85f007b7-540e-0410-9357-904b9bb8a0f7
* More standard layout for \lambda in chapter CIC.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15707 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
* Version number, copyright, credits: missing updates.Gravatar herbelin2011-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Html page titlesGravatar pboutill2011-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une feuille de style pour les définitions spécifiques à Hevea + ↵Gravatar notin2010-06-23
| | | | | | divers corrections sur la génération du manuel de référence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ↵Gravatar notin2010-06-23
| | | | | | coq.inria.fr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification du style du manuel de référenceGravatar notin2009-02-11
| | | | | | (cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated datesGravatar herbelin2009-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
| | | | | | | | | | | | the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 15:36:53 +0000