| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This was mentioned in #5631 as well. Now, forall, fun
and casts have index entries.
|
|
|
|
|
|
|
|
|
|
Cf CHANGES for details.
|
|
|
|
emphasized
|
|
"@qualid pattern".
|
|
"constructor" and "inductive" are meant also.
|
|
|
|
This commit also removes comments from Coq examples, as they cause
extraneous delayed prompts that clutter the output because coq_tex cannot
remove them. Some documentation errors were also fixed in the process,
since they are easier to spot now that only unexpected failures stand out.
|
|
|
|
|
|
Schemes] option.
|
|
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@16369 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 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
|
|
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
|
|
- 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
|
|
favour of 'co-inductive'.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to 2003.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
it properly in the syntax of terms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14522 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14425 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@12322 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
|
|
- Improved warning when found several path to the same file in path
[mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
[Datatypes.v, tactics]
PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des théorèmes prouvés par récursion ou corécursion mutuelle.
Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 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
|
|
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
When the system accepts a fixpoint, it now prints which decreasing argument
was used, e.g:
plus is recursively defined (decreasing on 1st argument)
The search is quite brute-force, and may need to be optimized for huge mutual
fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback.
N.B. in the standard library, only 4 functions have an decreasing argument
different from the one that would be automatically infered:
List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind
And compiling with as few explicit struct as possible would add about 15s
in compilation time for the whole standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 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
|
|
from commands about headers; where appropriate, surrounded those by
%BEGIN LATEX ... %END LATEX. Removed some \newcommands that were
ignored. Removed redefinitions of \land, \lor, \lnot: there are nicely
handled by Hevea.
Split headers.tex file into headers.sty (for LaTeX) and headers.hva
(for Hevea). This allowed removing comments like %BEGIN LATEX and %HEVEA
and also commands \makeatletter, \makeatother.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dans extensions de Gallina. Divers. (report revisions 9614 et 9594 de
la branche 8.1 vers le trunk)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9615 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
