| Age | Commit message (Collapse) | Author |
|---|
|
This makes queries like Print or Extraction block and not
raise the error "the value is not ready". This should make
CoqIDE work for every kind of script.
|
|
This commits makes the concept of delegated and async more orthogonal.
A proof can be async but not delegated to a worker (if it is known
to be very small it is too much overhead to delegate to a worker).
A proof that is not async cannot be delegated to a worker.
An async proof that contains an error does not prevent Coq from continuing
the execution (interactive mode) and can be fixed without invalidating
the whole document (CoqIDE knows how to do that) even if it is processed
locally. It used to be the case only for delegated proofs, now it worker
for all the proofs that can be in principle delegated (doing it or not
is an implementation detail, an optimization).
|
|
|
|
|
|
Thanks the the previous patchset a worker can be asked to send
back "light" version of the system states. This is reasonably
efficient hence the idea of letting a worker hang around just to
hold system states for retrieval on demand is dropped.
|
|
|
|
|
|
|
|
|
|
|
|
API to let one forge a frozen state out of another frozen state
plus some frozen bits
|
|
In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
|
|
A Dyn.t boxes a type tag with the original object, so calling
== on the Dyn.t does not work, hence this extra API.
|
|
|
|
|
|
have x permission"
This reverts commit 607503b28fca50f4b76b2237d5ca13802b8252fa.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
|
|
This is the second part of the Exninfo patch. It introduces dependency in
the Thread library in all Coq files.
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.
|
|
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
|
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
|
|
|
|
step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.
At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.
|
|
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
|
|
unification flags (see also temporary revert in d083200ae5b).
|
|
|
|
|
|
|
|
twice). Thanks to Marc Lasson for spotting this.
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
|
|
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
|
|
for typeclasses.
This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.
Fixes #3841.
|
|
This makes such things work:
x:nat
h: x = 3
================
True
Search x.
|
|
|
|
|
|
|
