| Age | Commit message (Collapse) | Author |
|---|
|
The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.
|
|
|
|
|
|
We know statically that only global references are passed to make_resolves.
|
|
|
|
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
|
|
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
Reviewed-by: SkySkimmer
|
|
It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.
Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
|
|
|
|
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.
|
|
|
|
|
|
|
