| Commit message (Collapse) | Author | Age |
... | |
| | |
|
| |
| |
| |
| |
| |
| | |
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
| | |
|
| |
| |
| |
| | |
variables and definitions in sections is unsupported.
|
| | |
|
| |
| |
| |
| | |
Fixpoint/Definition.
|
| |
| |
| |
| |
| | |
(let x := t in u) a that should be reduced. Maybe a different
decomposition/reduction primitive should be used instead.
|
| |
| |
| |
| |
| | |
It was not detected because of a "bug" in clear checking the existence
of the hypothesis only at interpretation time (not at execution time).
|
| |
| |
| |
| |
| |
| |
| | |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| |
| |
| |
| |
| | |
- Fixing dead code, doc.
- Relaxing constraints on using an as-tuple in inversion.
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.
Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".
Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).
See file induct.v for effect of changes.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
|
| |
| |
| |
| | |
Following a discussion on coq-club on Jan 13, 2016.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
We can now use the expressivity of GADT to work around historical kludges
of generic arguments.
|
| |
| |
| |
| |
| |
| | |
No more Obj.magic in Genarg. We leverage the expressivity of GADT
coupled with dynamic tags to get rid of unsafety. For now the API
did not change in order to port the legacy code more easily.
|
| | |
|
| |
| |
| |
| | |
This will allow an easier landing of the rewriting of Genarg.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
In particular, documenting bracketing of last pattern on by default.
|
| |
| |
| |
| |
| |
| |
| | |
- Being stricter on the ordinal suffix accepted (only st for 1, 21,
etc, nd for 2, 22, etc., etc.)
- Reporting when the suffix is not the expected one (rather than
considering that, e.g. 2st, is two tokens, a number then an identifier).
|
| |
| |
| |
| |
| |
| |
| |
| | |
The term "assumed" refers more to the type of the object than to the
name of the object. It is particularly misguiding when P:Prop since P
is assumed would suggest that a proof of P is assumed, and not that
the variable P itself is declared (see discussion with P. Castéran on
coqdev: "Chapter 4 of the Reference Manual", 8/10/2015).
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|