| Age | Commit message (Collapse) | Author |
|---|
|
This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
|
|
Only one field was used throughout the code base.
|
|
|
|
|
|
|
|
The code below checks that the term is an applied equality, so allowing
non-trivially quantified inductive types would trigger an error right after.
|
|
In this mess of higher-order callbacks it helps sorting out the invariants
of the structure.
|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
We move the "verbose" case to the only point it is actually used.
It is a bit unfortunate since it implies a bit of code duplication, but
this should not affect runtime since the replaying only happens in case
of a user-facing warning.
|
|
Fix #12944
|
|
The names computed in consume_pattern were lost when calling
intros_pattern_core. Moreover, the computation of names to avoid was
done several time. We compute it once for all.
|
|
No reason to have them there.
|
|
It makes no sense to call the context from the goal "global"
|
|
Fix #12928
Fix #3146
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
|
|
|
|
We try to encapsulate the future goals abstraction in the evar map.
A few calls to `save_future_goals` and `restore_future_goals` are still
there, but we try to minimize them.
This is a preliminary refactoring to make the invariants between the
shelf and future goals more explicit, before giving unification access
to the shelf, which is needed for #7825.
|
|
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
|
|
|
|
Fix #12676
|
|
recognition.
Reviewed-by: mattam82
|
|
of artificial dependencies disappearing by reduction
Reviewed-by: ppedrot
|
|
|
|
We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
|
|
We know statically that it is going to be the one provided at the time of
lookup, so we simply fetch it from there.
|
|
|
|
The two implementations are essentially the same except for potential
interleaving of let-bindings and pattern-matchings. The only place
the removed function was called probably does not rely on this difference
of behaviour.
|
|
Instead of having to go through the pattern translation, we compute the
pattern directly from the term.
|
|
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
|
|
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
As suggested by Laurent Thery to Chris Dams on Coq-Club.
(And fix the documented syntax in the manual.)
|
|
purely applicative stacks
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.
The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.
A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
|
|
The old code was refreshing the whole evarmap when only the constraints
introduced by the term would matter. Since exact hints never introduces
metas for missing binders, there is nothing to extract from the clenv,
so we can just generate a fresh universe substitution.
|
