| Age | Commit message (Collapse) | Author |
|---|
|
a context.
Reviewed-by: mattam82
|
|
Reviewed-by: ppedrot
|
|
|
|
We use higher-level combinators instead of composition of low-level ones.
|
|
The boolean assumedly used to cut recursion was always set to true, since
its introduction in 64ac193.
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
|
|
The previous implementation appears to be sound when Mangle Names is
off, but it relies on two fragile assumptions, namely that
next_global_ident_away always returns different identifiers when called
with naming hints which are different after stripping all digits from
the end, and that default_id_of_sort (locally defined) never returns
"HC" or "P", or either of those followed by a string of digits.
These changes make both assumptions unnecessary.
As a side note, it seems odd that fresh is ignoring it's env parameter.
|
|
In case we give an empty list of occurrences to e_change_in_hyps, we
can return immediately. This saves the allocation of a dummy evar, and
a O(n) map over the context for "local" reduction functions.
Note that passing an empty list of hypotheses is the default for both
the "change" tactic and reduction tactics.
|
|
from initial evars
Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
|
|
|
|
comment in #12944).
Ack-by: RalfJung
Ack-by: jashug
Reviewed-by: ppedrot
|
|
The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.
This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.
Also fixes bugs #4095 and #4413.
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
|
|
Reviewed-by: herbelin
|
|
Once again, we now statically the type of the argument is the same, so there
is no need to call the old unification.
|
|
|
|
The clenv was generated to eliminate a negation, but its argument was given
immediately and its type statically known to be the same.
|
|
|
|
Actually the callers of that function only apply it to an applied
inductive type.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
Ack-by: SkySkimmer
Ack-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
|
|
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())`.
|
