| Age | Commit message (Collapse) | Author |
|---|
|
|
|
per @aspiwack's comments in [this pull request
review](https://github.com/coq/coq/pull/940).
|
|
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
|
|
As suggested by @psteckler.
|
|
|
|
|
|
|
|
|
|
|
|
It has been deprecated for a while in favor of `Qed`.
|
|
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.
|
|
|
|
The V7 to V8 translator lost part of term annotations.
|
|
|
|
|
|
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).
|
|
|
|
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
|
|
- 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
|
|
- 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
restructuration du répertoire de documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
