| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
choice
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Further highlighting when the correspondence between variants of
choice is independent of the domain and codomain of the function, as
was done already done in the beginning of the file (suggestion from
Jason).
Adding some corollaries.
|
| | | |
|
| | |
| | |
| | |
| | | |
Also integrating suggestions from Théo.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
axiom of choice (i.e. choice on setoids) and of the axiom selecting
representatives in classes of equivalence.
Also integrating suggestions from Théo.
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
choice of a representative in a partition of bool.
Also move a result about propositional extensionality from
ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by
symmetry.
Also spotting typos (thanks to Théo).
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Don't know if compare_cont is very useful to use, but, at least, these
extensions make sense.
|
| |/ /
|/| |
| | |
| | | |
This completes the series and cannot hurt.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| | |
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
|/
|
|
|
|
|
|
|
| |
- Do not use induction/elim when not necessary: use destruct or
destructive intro-pattern instead.
- Do not use heavy automation when lightweight automation is enough.
- Prefer shorter proofs when it does not hinder readability.
- Do not rely on automatically generated names.
- Use bullets.
|
| |
|
|\ |
|
| |
| |
| |
| |
| | |
Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
|
| | |
|
|\| |
|
| |\
| | |
| | |
| | | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | |
|
| |\ \
| | | |
| | | |
| | | | |
Was PR#336: Remove v62
|
| | | |
| | | |
| | | |
| | | | |
Some options are expected to be deprecated
|
| |/ /
| | |
| | |
| | |
| | | |
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
|
| |/ |
|
|\| |
|
| |
| |
| |
| | |
I've messed up with parts of the compatibility files I had to commit.
|
| |\ |
|
|\| | |
|
| |\ \ |
|
| | | | |
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | | |
A file was introduced by mistake in theories/Logic.
|
|\| | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
|
| | | | |
|
|\| | | |
|
| | |/
| |/|
| | |
| | |
| | |
| | |
| | | |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| | | |
|
|\| | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
Importing VectorNotations breaks `; []`. So we make sure it's not
imported by defualt. Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
|
| | |
| | |
| | |
| | |
| | | |
Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
|
|\| | |
|
| | | |
|