| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| | |
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|/ |
|
|\ |
|
| | |
|
|/
|
|
| |
Includes fixes and suggestions from Théo.
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| | |
This makes the following work correctly:
make only TGTS="foo bar" -j2
note that
make foo bar -j2
is not doing what you think
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:
```
Goal Type.
⋮
Save id.
```
has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.
We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.
It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
|
|/
|
|
| |
It has been deprecated for a while in favor of `Qed`.
|
|
|
|
|
| |
We seized this opportunity to do a little refreshing of the section
describing injection.
|
|\ |
|
|\ \ |
|
| | | |
|
| | | |
|
|\ \ \ |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This commits documents the as clause of specialize and that the
as clause of pose proof is optional.
It also mentions a feature of assert ( := ) that was available
since 8.5 and was mentionned by @herbelin in:
https://github.com/coq/coq/pull/248#issuecomment-297970503
|
|\ \ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
let-ins
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
As per Enrico's request.
|
| |_|/ /
|/| | | |
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
record fields.
|
| | | | | |
|
| | | | | |
|
| |_|/ /
|/| | |
| | | |
| | | | |
Since About mentions it the doc should as well.
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
off by default
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Supporting let-ins in tactic "fix", and hence in interactive
Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
presence of let-ins.
|
|\ \ \ \ |
|
| | | | | |
|
| |/ / /
|/| | | |
|
|\ \ \ \ |
|
| |_|/ /
|/| | |
| | | |
| | | |
| | | | |
And an extra minor changes (use of zeroone when relevant, use of type
rather than term).
|
|\ \ \ \ |
|
| | | | | |
|
|\ \ \ \ \ |
|
| |_|_|/ /
|/| | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Maxime points out that -notop cannot be used as the kernel requires
all constants to belong into a module. Indeed:
```
$ rlwrap ./bin/coqtop -notop
Coq < Definition foo := True.
Toplevel input, characters 0-23:
> Definition foo := True.
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: No session module started (use -top dir)
Coq < Module M. Definition foo := True. End M.
Module M is defined
Coq < Locate foo.
Constant If you see this, it's a bug.M.foo
(shorter name to refer to it in current context is M.foo)
```
My rationale for the removal is that this kind of incomplete features
are often confusing to newcomers ─ it has happened to me many times ─
as it can be seen for example in #397 .
|
|\ \ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | |
|