| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
local definitions...
|
|
|
|
|
|
|
|
|
|
parameters.
|
|
Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
|
|
irrelevance.
Application of previous commit in Hurkens.v.
|
|
In particular there is no retract of the type of negative propositions in a negative proposition.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
|
|
|
|
For consistency with ChoiceFacts
|
|
The generalized versions are names *_one_var. We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.
This closes the rest of Bug 3019, and closes pull request #6.
|
|
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).
|
|
new files (WeakFan.v and WKL.v).
|
|
Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.
|
|
|
|
|
|
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
|
|
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
|
|
|
latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.
- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-
|
