| Age | Commit message (Collapse) | Author |
|---|
|
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
|
|
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
|
|
|
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
|
|
|
|
|
|
|
|
|
Set Printing Existential Instances (see bug report #3951).
|
|
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
|
|
Updated doc, but not tests-suite yet.
|
|
Error messages were outdated.
|
|
|
|
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
Also started a preliminary documentation about evars (where to have it
in the doc is somehow open).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16234 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@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15654 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
environment to display the example.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.
It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Even if they are no-ops now, the commands Set/Unset Undo themselves
are kept for compatibility, in particular to avoid error messages
or warnings during the initialization of ProofGeneral.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 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@10479 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@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
iter_constr_with_full_binders + documentation de Guarded.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/doc/refman/RefMan-pro.tex
M trunk/pretyping/inductiveops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9799 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@9286 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
légère restructuration autour de Proof with et Hint Rewrite + maj crédits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 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
|
