| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Compared to the original proposition (01f848d in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
| | |
|
| | |
|
| | |
|
|/ |
|
|\
| |
| |
| | |
work better on them
|
| |
| |
| |
| |
| | |
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|/ |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
| |_|/
|/| | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an
unexpected extra dependency due to a name collision with a section
variable.
|
| |/
|/|
| |
| | |
Fixes Coq bug 5635 (https://coq.inria.fr/bugs/show_bug.cgi?id=5635).
|
| | |
|
| | |
|
| | |
|
|/ |
|
|\ |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| | |
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607).
PR #220 put the exports in the wrong compat files, presumably because it
was originally targeted to version 8.6, and this wasn't updated when it
was retargeted to version 8.7.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
(for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
- wrong -for-pack used for their inner .cmx
- dependency over modules not provided (for instance Tacenv, that ends
up being a submodule of the pack ltac_plugin).
But we were lucky, those files were actually never loaded, thanks to the
several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
and hence tell Coq that these modules are already known, preventing
any attempt to load them.
Anyway, this commit cleans up this mess (thanks PMP for the help)
|
|\ \
| |/
|/| |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
| | | |
|
| |/
|/| |
|
|\ \ |
|
|\ \ \ |
|
| |/ /
|/| |
| | |
| | |
| | |
| | | |
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
| | | |
|
| |/
|/| |
|
| |
| |
| |
| | |
automatically instead
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
| |
| |
| |
| |
| | |
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
|
| |
| |
| |
| |
| | |
Forwards/backwards reasoning thoughts come from
https://github.com/coq/coq/pull/385#discussion_r111008347
|