| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
|/
|
|
| |
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 .
|
|\ \ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | |
|
| |/ / /
|/| | | |
|
| |/ /
|/| |
| | |
| | |
| | | |
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
|/ / |
|
|\| |
|
| | |
|
|\| |
|