| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
|
|
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
We tweak the message a bit.
|
|
|
|
They were not used anywhere anymore.
|
|
This was useless, since we did not observe the difference on evars.
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
|
|
|
The real list is computed by tok_using in CLexer.
|
|
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.
Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
|
|
We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
|
|
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
|
|
This is to be compatible with the possibility of having non truly
recursive fixpoints.
|
|
|
|
remove itself in the set of elements bigger than it if it is indeed
the case.
This does not impact the warning issued when the recursivity is not
mutual but this produces a result consistent with the unary case when
the order is reflexive (i.e. results of the form (x,Inr[x,y]) happens
also in the mutual case to indicate a cycle x<=y<=x while before we
had results of the form (x,Inr[x]) only in the unary case). I.e.:
Before:
(x,[y]),(y,[x]) -> (x,Inr[]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
Now:
(x,[y]),(y,[x]) -> (x,Inr[x]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
Some comments referred to the old way of redeclaring constants at section
closure. One of the comments was almost 20 years old...
|
|
This encapsulates better the invariants of this function.
|
|
It was trying to warn the user about missing schemes. Since find_scheme was
generating those constants anyways, this was never reached.
|
|
Ack-by: ejgallego
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: jfehrle
|
|
|
|
|
|
Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.
We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.
|
|
Close #12192
Also removed transforming arbitrary exceptions into Faulty to make it
easier to reason about exception flow
|
|
The reason for which the code was written this way is probably historical. In
the current implementation, we read the marshalled data exactly once by library,
thus there is no gain from delaying.
|
|
|
|
|
|
|
|
See CEP#44 for futher details.
|
|
Closes #12177.
|
|
Reviewed-by: ppedrot
|
|
line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
|
|
This is an internal function for scheme declaration handled properly
now, we can also remove `pure_definition_entry` which is IMO good too.
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
