| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
of the Reference Manual.
|
| |
| |
| |
| | |
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
|
| |
| |
| |
| | |
the formatting and renamed the tactics to match modern naming conventions.
|
|/
|
|
| |
Manual.
|
|\
| |
| |
| | |
and 'Tactics' of the Reference Manual.
|
|\ \ |
|
| | | |
|
|/ / |
|
| | |
|
|/
|
|
|
|
|
| |
commands', 'Proof handling' and 'Tactics' of the Reference Manual.
Fixed some more serious errors related to tactics functional induction, unfold, hnf and red.
Added some error messages and remarks for tactics btauto, rtauto and red.
|
|\ |
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
language' of the Reference Manual.
|
| | | |
| | | |
| | | |
| | | | |
of the Reference Manual.
|
|/ / /
| | |
| | |
| | | |
Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
|
|\ \ \
| | | |
| | | |
| | | | |
case of missing record field
|
| |/ /
|/| |
| | |
| | |
| | |
| | |
| | | |
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like
`Global Set SsrHave NoTCResolution`. I don't think it is needed (just
let the user write the desired locality), but if it is, the right way of
doing it is to let clients of Goptions specify a default locality.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |_|_|/ / / /
|/| | | | | |
| | | | | | |
| | | | | | | |
As stated in the manual, the fourier tactic is subsumed by lra.
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
The changed QuestionMark structure breaks Coq-Equations.
Add an overlay to fix this.
|
| |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|\ \ \ \ \ \ |
|
|/ / / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This way, when editors leave over temporary files from editing
user-overlays, we don't prevent commits unless they are added to git.
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Fixes #8067. This is becoming the default in many developments, so it
makes sense to require it too, both for Coq and for Plugins.
|
|/ / / / / /
| | | | | |
| | | | | |
| | | | | | |
Catched by compiling the ml files from ml4.
|
|\ \ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
the Reference Manual (Introduction, Credits).
|
| | | | | | | |
|
|\ \ \ \ \ \ \ |
|
|/ / / / / / /
| | | | | | |
| | | | | | |
| | | | | | | |
We turn all Coq warnings that are on by default into errors.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This is much more efficient than using Nativevalues.is_accu function which
incurs a lot of irrelevant checks on its argument.
|
| | | | | | | |
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
No need to roll up a new data structure when Environment has O(log n) add
and lookup of rel definitions.
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Manual (Introduction, Credits).
|
|\ \ \ \ \ \ \
| |_|_|/ / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \
| |_|/ / / / /
|/| | | | | | |
|
| |_|_|_|/ /
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|\ \ \ \ \ \ |
|
| | |_|_|/ /
| |/| | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
See https://github.com/ocaml/num/issues/9
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
flambda happy.
See issue #8043.
Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like
an OCaml bug.
|
| |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | | |
As discussed in #6930, we remove the warnings jobs and instead do
require the developers to submit a clean build.
|
|\ \ \ \ \
| |/ / / /
|/| | | | |
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|