| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
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.
|
| | |
| | |
| | |
| | |
| | | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
|/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.".
|
|
|
|
|
|
|
|
|
|
| |
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
|
| |
|
|\ |
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | | |
(Universes and Evd)
|
| | |
| | |
| | |
| | | |
Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
|
| | | |
|
| | | |
|
| |/
|/| |
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | | |
It was forcing the macro to generate code that was useless.
|
| |/
|/| |
|
|\ \
| | |
| | |
| | | |
points of Camlp5
|
| |/
|/|
| |
| | |
Don't allow notations attached to uniform inductives
|
|\ \
| | |
| | |
| | | |
Z into three files
|
| | |
| | |
| | |
| | | |
Fixes #7857.
|
| | | |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| | |
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
|
| | |
|
|\ \
| |/
|/| |
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
constants
|
| |/ /
|/| | |
|
| | |
| | |
| | |
| | |
| | | |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a first step towards the acceptance of mutual record types in the
kernel.
|
| | | | | |
|
| | |/ /
| |/| |
| | | |
| | | |
| | | | |
- we always rename
- we compile {clear}/view to /view{clear}
|
| | | | |
|
|/ / / |
|
| | |
| | |
| | |
| | |
| | | |
We only use it locally, so we simply register the ML tactic inside the module
but we do not export the syntax.
|
| |/
|/|
| |
| |
| |
| | |
The code was wrong as it relies once again on term equality and fails
on polymorphic constants. Quote is bound to disappear, so we write a
correct version of this 10-line function in setoid_ring.
|
|/
|
|
|
|
|
|
|
| |
I think the bug was introduces when apply_type was made safe.
In the test joint to #7255 rewrite (setoid case) generates an
ill-typed goal and apply_type raises a Pretype_error.
It is unclear to me why the tactic monad does not turn the
pretype_error into a UserError
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | | |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
| |/
| |
| |
| |
| |
| |
| |
| | |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|