| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
reference manual.
|
|
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.
|
|
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).
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ s/cbv/lazy of bug 2542
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Beware! after this, a ./configure must be done. It might also
be a good idea to chase any phantom .vo remaining after a make clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12815 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
|
|
- 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
|
|
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
|
|
(Cachan/IntMap)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Chapter
Remplacement pageref par ref parce que pageref n'a pas de sens pour
la version HTML
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9784 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
immediately follow sectioning commands insides those sectioning commands.
If \label{...} is placed after \section{...}, then, when clicking on the
link in the HTML file produced by Hevea, we are moved to the correct
section, but the section header is just above the screen. Hevea manual
recommends writing \section{...\label{...}} and similarly for index.
On the other hand, writing commands inside the argument of sectioning
commands is potentially dangerous because these arguments are reproduced
not only to produce the section header but also to produce headers
and/or table of contents entries. Thus, \index{...} and \labels{...} may
be executed several times. Indeed, if we put a \typeout{...} instruction
inside the argument to a sectioning command then it will be executed,
besides the section itself, in the table of contents and once for every
appearance of the header.
However, it seems that the \label command are not executed several times
unless they are prefixed with \protect, and \index command is not
executed multiple times even then. So maybe it's OK to put \label and
\index inside sectioning commands.
When hyperref package is used, the \newlabel command left in .aux file
has an extra group {...} which includes another \label command! This may
lead to trouble when we use \nameref (?).
However, the most reliable way would be to use the optional argument of
sectioning commands. Then the text only goes to the optional argument and
the text plus \label plus \index goes to the main argument. The optional
argument is used for headers and table of contents. This works fine with
Hevea as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9312 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9207 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 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
|
