| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
section variable.
For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
|
| |
|
|
|
|
|
| |
Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.
Had to fix a few occurrences in std lib.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
finite set libraries.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
| |
|
|
| |
local definitions...
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
équation;" which was committed by mistake.
This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
|
| | |
|
| |
|
|
| |
parameters.
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| |
|
|
|
| |
projections and regular records.
Easily fixable backwards incompatibility.
|
| |
|
|
| |
Thanks to Yves for reporting it!
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
| |
|
| |
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.
|
| |
|
|
| |
experiments about computing PI
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
|
| |
|
|
|
| |
Left a README, just in case someone will discover the remnants of it
decades from now.
|
| | |
|
| |
|
|
| |
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).
|
| | |
|
Arnaud Spiwack
Maxime Dénès
Sébastien Hinderer
Pierre Letouzey
Hugo Herbelin
Guillaume Melquiond
Matthieu Sozeau
Pierre Boutillier
Yves Bertot
Pierre-Marie Pédrot
Jason Gross