| Age | Commit message (Collapse) | Author |
|---|
|
|
|
unification algorithm in consider_remaining_unif_problems. If it
happens to be problematic, one can backtrack to the "optimization"
from 3bd9cb26b which has a restriction on rels/vars.
|
|
|
|
following working:
Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
|
|
|
|
hidden behind another notation.
|
|
initial segment of the context of the evar.
|
|
|
|
|
|
|
|
|
|
|
|
section variable.
For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
|
|
After commit b46944e the system got way slower, hence the optimization
is relevant also for non polymorphic constants. Putting it back now,
but we shall find something in between: an optimization that does
not clash with async proofs but that gives some performance improvement
over no optimization at all.
|
|
As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.
But it is better than nothing I guess.
|
|
|
|
Before this commit the worker was sending back a proof term
as built by tactics. The master receives the proof terms and
eventually (when one clicks on the gears in CoqIDE) check it
with the kernel. This meant that errors like the ones produced
by the "fix" tactics were discovered very late.
Now a worker checks with its kernel the proof term before sending it
back. The term is also checked by the master, eventually, but the
error is signaled early.
|
|
|
|
|
|
Given that the proof state contains a callback (a terminator)
that is not sent (dropped by the ephemeron mechanism at marshall
time) de-referencing the ephemeron during this function makes it
impossible to call it in a worker. Now the worker can call the
function and replace the terminator with a good one.
|
|
|
|
Before the union was performed as a UContext.t union, that
concatenates the instances arrays, while one wants to avoid
duplicates.
We also assert that polymorphic constants have all constraints
in the constant_body (field const_universes), since the extra body
univs (stored in the opaque tables) are just for regular constants
processed asynchronously.
|
|
Such printer is already in Termops
This reverts commit 5d6106a075b79abbb92b03bbca7b13a517cf4925.
|
|
|
|
|
|
|
|
When one generates a .vi file only the type is stocked.
When one completes a .vi the proof term is stocked but the
corresponding type is not changed:
- if one minimizes the constraints of the body, the minimization
could find that 2 univs are equal and substitute one for the
other in the body, but it should also apply the subst to the type
orelse coqchk could fail
- also, a "retroactive" change of a type (making it stricter)
invalidates what was type checked afterwards, so this operation
clashes with the vi2vo compilation chain
Hence we enable this optimization only for universe polymorphic
constants that:
- are the ones that truly requires such optimization
- are never processed asynchronously, so the scenario above does
not apply
|
|
|
|
I find it very odd not to have a pretty printer for terms than can
be called from *everywhere*. This commit sticks in Term a long spaghetti
to let Printer install a printing function.
|
|
|
|
Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.
Had to fix a few occurrences in std lib.
|
|
removing the need of thread creation in the interface.
|
|
|
|
|
|
|
|
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
|
|
|
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|
|
|
|
Still unsure about .o file (should they be shipped for the native_compute
machinery or .cmxs suffice?)
|
|
PIDE based user interfaces use glob files and source files to
implement hyperlinks
|
|
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
|
|
environment.
A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly)
I'm not quite sure why it caused #3679, though. But it still seems to be solved.
|
|
The validation process was passing most of its time in the construction of
the name of the current context.
|
|
|
|
|
|
|
|
|
|
accidentally mixed up in 9aa416c0c6.
|
|
|
