| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.
This fixes #6313.
Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
|
|
|
|
|
|
|
|
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
|
|
|
|
|
|
|
|
|
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
|
|
|
|
|
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
|
|
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
|
|
|
Before sometimes there were lists and strings.
|
|
|
|
Note the problem with `create_evar_defs`.
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
|
|
|
|
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
|
|
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
|
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
|
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
|
|
|
|
|
|
|
Use an explicit label ~algebraic for make_flexible_variable as well.
|
|
|
|
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
|
|
Now it is a private field, locations are optional.
|
|
|
|
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.
Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.
Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
|
