| Age | Commit message (Collapse) | Author |
|---|
|
|
|
pattern
Reviewed-by: ppedrot
|
|
|
|
|
|
We compute earlier if "apply in" clears or not.
We inline prepare_naming into its only client prepare_intros_opt
(using the more general make_naming instead).
|
|
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.
|
|
This was a source of slowdown observed in bedrock2.
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
|
|
|
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
|
|
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
|
