| Age | Commit message (Collapse) | Author |
|---|
|
check resolution of evars more incrementally
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ppedrot
|
|
incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
naming
Ack-by: gares
Reviewed-by: ppedrot
|
|
Also some dead code.
If no typo is introduced, there should be no semantic changes.
|
|
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
|
|
|
