| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #4988.
|
|
|
|
not "first [ progress tac1 | progress tac2 ]".
And add a missing backslash.
|
|
|
|
|
|
|
|
|
|
I also renamed the type to nattree (see discussion on
https://github.com/coq/coq/pull/5979) to disambiguate from another,
earlier example.
|
|
Bug description:
The "now" tactic, which is being used in the standard library,
is not documented in the Reference Manual
This commit documents the easy tactic, and gives now
as a variant.
|
|
Made a description of unfold...in and moved the index entry there.
|
|
This was mentioned in #5631 as well. Now, forall, fun
and casts have index entries.
|
|
As discussed in the bug report, this adds `(...) and `{...} to the
index.
|
|
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
|
|
|
|
|
Also simplifies the way it is presented (no need to be overly precise).
|
|
to escape non-UTF-8 file names)
|
|
|
|
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
