| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
|/
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
|
|
|
|
| |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
|
|
|
| |
We move the last 3 types to more adequate places.
|
|
|
|
|
| |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
|
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |
|
| |
|