| Age | Commit message (Collapse) | Author |
|---|
|
Just hoisted a definition out of a loop. Not that this part of the code is time critical at all. I just feel it's cleaner.
|
|
Instead of filtering over the goals we have just creating and running through the evar_map, fetching the evar_info (that we've just created), and marking it as unresolvable, the goals are just created unresolvable. Which is probably what I should have done from the beginning, but it had escaped my notice during my code-cleaning session.
|
|
I can't say I condone having unsafe primitives which are not used anywhere. But if they are to be there, let's make sure they don't duplicate code.
|
|
full instances.
|
|
|
|
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
|
|
|
|
|
|
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
|
|
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
|
|
arbitrary direction as if it were an "evar = evar" problem.
|
|
Incidentally, this allows to make earlier the collapse of CUMUL to
CONV when force is true.
|
|
evar_define.
Interestingly, the added choose in evarconv.ml allows solve_evar_evar
to be observationally commutative, in the sense of not either fail or
succeed in compiling the stdlib whether problems are given in the
left-to-right or right-to-left order.
|
|
subsumed by the call to project_evar_on_evar.
|
|
normalize it afterwards.
|
|
In particular, the old hypinfo is made as a proper cache, preventing dynamic
tricks to decide whether it was rightful to refresh it.
|
|
|
|
|
|
|
|
|
|
env.
|
|
This allows to have the example in test setoid_unif.v to work again.
|
|
|
|
automatic refinement of instances, thus failing when provided with
an incomplete term instead of silently lauching the proof mode.
|
|
|
|
|
|
|
|
|
|
|
|
The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
|
|
|
|
|
|
When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.
Fixes test-suite/success/apply.v
|
|
Closes #3801.
|
|
If the async-proofs-always-delegate is passed, workers are killed
only when the proof they computed is obsolete. If one jumps back
to a state that was computed by the worker (and not the master) instead
of (re)computing such state in the master ask the worker to send it
back.
|
|
|
|
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
|
|
|
Even indirectly, if it depends on another state that in turn failed.
|
|
|
|
|
|
|
|
|
|
|
|
When async_proofs_always_delegate is on, park proof workers and
dispatch to them queries. This flips the current way of printing
goals in PIDE base UIs: it is not the worker that prints all goals
while coomputing the states (and the dies), it is the UI that asks
for them when they are under the eyes of the user.
|
|
Generalize the old model by letting one park a worker and
by letting the (parked) worker be picky about the tasks it
picks up.
The use of that is the following: a proof worker, while performing
its "main" task (building a proof term) computes all the intermediate
states but returns only its main result. One can ask the worker
to hang around, and react to special tasks, like printing the
goals of an intermediate state.
|
|
This lets me have a pool of active workers of a fixed size,
plus a parking area where workers that completed their job
can stay holding their state (and eventually one can ask them
to query such state afterwards).
|
|
E.g. let a worker pick up only jobs he is able to deal with.
|
|
The default hook value is the one used by CoqIDE
|
|
|
