| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| |/
|
|
|
| |
Note that one of them is in the name of the main theorem, so we use a
compatibility notation.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
| |
As explained in BZ#5713 report, the requirement for a non-empty
context is not needed, so we remove it.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Shortnames and natural language descriptions of principles are moved
next to each principle.
The table of contents is moved to after the principle definitions.
Extra definitions are moved to the definition section (eg DependentFunctionalChoice)
Compatibility notations have been moved to the end of the file.
Details:
The following used to be announced but were neither defined or used,
and have been removed:
- OAC!
- Ext_pred = extensionality of predicates
- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop
GuardedFunctionalRelReification was announced with shortname GAC! but
shortname GFR_fun was used next to it. Only the former has been retained.
Shortnames and descriptions have been invented for
InhabitedForallCommute DependentFunctionalRelReification
ExtensionalPropositionRepresentative ExtensionalFunctionRepresentative
Some modification of headlines
|
| | |
|
| |
|
|
|
|
| |
This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The "theories/Logic/PropExtensionalityFacts.v" file was:
- compiled
- used in several places
but not actually installed.
This commit fixes that.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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).
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Hurkens.v by dropping the artificial need for monad laws. Tactic eauto
decided to be dependent on the laws but there is a shorter proof
without them.
[Interestingly, eauto is not able to find the short proof. This is a
situation of the form
subgoal 1: H : ?A |- P x
subgoal 2: H : M ?A |- M (forall x, P x)
where addressing the second subgoal would find the right instance of
?A, but this instance is too hard to find by addressing first the
first subgoal.]
|
| | | |
|
| |/
|
|
| |
because P:U->Prop implies P:U->Type, the new statement is strictly more useful.
No change was needed to the proof.
|
| |\ |
|
| | |
| |
| |
| |
| | |
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
|
| |\| |
|
| | |
| |
| |
| | |
A file was introduced by mistake in theories/Logic.
|
| |\| |
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
| |
extensionality in H supposed to be a quantified equality until
giving a bare equality.
Thanks to Jason Gross and Jonathan Leivent for suggestions and
examples.
|
| | |
|
| |
|
|
|
|
| |
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
| |\ |
|
| | |
| |
| |
| | |
variables and definitions in sections is unsupported.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
| |\| |
|
| | |
| |
| |
| | |
Marking it as experimental.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
In particular, a proof of the equivalence of excluded-middle and an
unrestricted principle of minimization.
Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
Pierre-Marie Pédrot
Hugo Herbelin
Vincent Laporte
Maxime Dénès
Théo Zimmermann
Jasper Hugunin
Pierre Letouzey
Gaetan Gilbert
Matej Kosik
Jason Gross
Abhishek Anand
Jason Gross
Matthieu Sozeau