| Age | Commit message (Collapse) | Author |
|---|
|
When restricting an evar with candidates, raise an exception if this
restriction would leave the evar without candidates, i.e. unsolvable.
- evarutil: mark restricted evars as "cleared"
They would otherwise escape being catched by the [advance] function
of clenv, and result in dangling evars not being registered to the shelf.
- engine: restrict_evar marks it cleared, update the future goals
We make the new evar a future goal and remove the old one.
If we did nothing, [unshelve tac] would work correctly as it
uses [Proofview.advance] to find the shelved goals, going through
the cleared evar. But [Unshelve] would fail as it expects only
undefined evars on the shelf and throws away the defined ones.
|
|
Avoid adding the same unification problem twice, module evar instantiation.
|
|
|
|
|
|
This API is a bit strange, I expect it will change at some point.
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
|
|
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.
|
|
|
|
|
