| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
Work done by Assia Mahboubi and Enrico Tassi
|
|
|
|
|
|
| |
We make it so that, by default, the HTML reference manual looks
like the one published online (same .css) and we provide a target
to serve it locally (requires python).
|
|
|
|
|
| |
And an extra minor changes (use of zeroone when relevant, use of type
rather than term).
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|\ |
|
| | |
|
|\| |
|
| | |
|
|/
|
|
| |
In particular, documenting bracketing of last pattern on by default.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
order to make it more concrete and more comprehensible.
This ver
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
| |
Updated doc, but not tests-suite yet.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
| |
To be continued someday, those style files are full of redundancies...
|
|
|
|
| |
documentation en ligne)
|
|
|
|
|
|
| |
documentation)
This commit r14895 comes apparently itself from commit r12010 in branch v8.2
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
CoInductive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14862 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
coq.inria.fr)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
|
|
| |
(cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
|