aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tutorial
Commit message (Collapse)AuthorAge
* Improve style slightlyGravatar Sam Pablo Kuper2017-08-01
| | | | | per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
* Replace jarring use of "Remark" with "Note"Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | | | | | or with nothing at all, to improve readability for native English speakers. Editors may wish to remove such constructions altogether in future revisions, per general style guidance such as: - https://en.wikipedia.org/wiki/Wikipedia:%22Note_that%22_is_unnecessary - https://english.stackexchange.com/a/238142/7318 - http://blog.apastyle.org/apastyle/2015/09/principles-of-writing-how-to-avoid-wordiness.html
* Mention again how to report bug and get version number.Gravatar Théo Zimmermann2017-06-30
| | | | As suggested by @psteckler.
* Better phrasing.Gravatar Théo Zimmermann2017-06-29
|
* More substance on discouraged practices.Gravatar Théo Zimmermann2017-06-29
|
* Some more corrections to the tutorial.Gravatar Théo Zimmermann2017-06-29
|
* Mask the reliance on coqtop.Gravatar Théo Zimmermann2017-06-29
|
* Update the Tutorial.Gravatar Théo Zimmermann2017-06-28
|
* [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | It has been deprecated for a while in favor of `Qed`.
* Fix some typos in tutorial (bug #5294).Gravatar Guillaume Melquiond2016-12-28
| | | | | | This commit uses the proper url for bug reporting, marks urls as such, stops qualifying the Coq'Art book as new, and fix the spacing after the Coq name.
* Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
|
* Fixing tutorial.Gravatar Pierre-Marie Pédrot2015-09-21
| | | | The V7 to V8 translator lost part of term annotations.
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* "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).
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
|
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 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
* - 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
* Updated datesGravatar herbelin2009-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
| | | | | | | | | | des inductifs à l'ordre supérieur par exemple) et qui sont de toutes façons accessible en contrib dans Rocq/CoC_History. - MAJ numéro de version dans Tutorial.tex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11232 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 petites modifs sur la docGravatar notin2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Maj du lien vers coq-bugs dans Coqide.Gravatar glondu2007-12-18
| | | | | | | On devrait mettre une redirection a l'ancienne adresse... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mention de coqide, proof general et pcoqGravatar herbelin2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enleve les commentairesGravatar cpaulin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des Makefile, ajout licences, corrections mineures suite àGravatar herbelin2006-02-23
| | | | | | | restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23
principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 11:34:58 +0000