| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
Talking about the difference between ident and pattern. Giving
examples.
|
| | |
|
| | |
|
| |
|
|
| |
Also simplifies the way it is presented (no need to be overly precise).
|
| | |
|
| |
|
|
| |
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
|
Hugo Herbelin
Gaëtan Gilbert
Théo Zimmermann
Matthieu Sozeau
Enrico Tassi
Guillaume Melquiond
Maxime Dénès
Pierre-Marie Pédrot
Matej Kosik
Pierre Courtieu
Pierre Letouzey
notin
gmelquio
herbelin
aspiwack
pboutill