| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Conflicts:
kernel/closure.ml
kernel/closure.mli
kernel/reduction.ml
|
|
Conflicts:
checker/closure.ml
checker/closure.mli
checker/reduction.ml
|
|
|
|
|
|
3cd718c, to the case of second_order_matching.
|
|
|
|
Updated doc, but not tests-suite yet.
|
|
Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
|
|
|
|
Error messages were outdated.
|
|
We reimplement a quick-n-dirty Gtk-free signal handler.
|
|
|
|
This allows a nifty display of the current state of the document through
a dedicated progress bar.
Also closes bug #3764.
|
|
|
|
Status of 335 and 3363 which are explicitly testing Require in modules
still to be addressed (to remove from test suite?).
|
|
not using the intended test. By fixing the intended test, the need for
a delta-expansion resulting from this commit in PFsection6.v (line
1255) of ssreflect disappears.
|
|
|
|
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.
|
|
|
