| Age | Commit message (Collapse) | Author |
|---|
|
Backported from a patch for v8.4 by Pierre Chambart. Part of the commit has been rendered obsolete by code reorganisation, leaving:
* OCaml runtime header files used to declare the int32, uint32, int64
and uint64 type. That got removed, and uses of those types should be replaced by the standard ones: uint32_t, int32_t, int64_t, uint64_t. Those are defined in stdint.h.
|
|
subproofs.
The front-end is supposed to take care of that, but it may help to catch bugs.
|
|
|
|
It was probably creating bugs when trying to use [escape].
|
|
I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command.
This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing.
Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end <block>` may close another block than intended if the number of unfocussing command executed is not the right one.
|
|
Backported from trunk.
|
|
As mentionne in #3969, using "once (constructor;tac)" leads in exponential blowups, whereas "[> once (constructor;tac) ..]" does not.
|
|
+ adjusting for the removal of `admit` by Arnaud Spiwack.
|
|
|
|
When lauching ideslave without configuring the communication channels,
instead of raising an anomaly which is never caught by the main loop, we
rather exit the process with a relevant error message.
|
|
After executing a command classified as VtProofStep the stm
prints the goals (if used via the tty API).
|
|
Admitted was not using the partial proof to infer discharged variables.
Now it does. The fix makes no sense, but restore the old behavior.
|
|
|
|
Admitted (like Qed) can be "partially executed", but is also unsafe.
|
|
|
|
|
|
|
|
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
|
universe-polymorphism mode.
|
|
|
|
|
|
|
|
seem to be overly strong in practice (see discussion related to #4035).
|
|
Not inventing a new fresh name if a non-fresh name is explicitly
given, as in v8.4.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit also removes comments from Coq examples, as they cause
extraneous delayed prompts that clutter the output because coq_tex cannot
remove them. Some documentation errors were also fixed in the process,
since they are easier to spot now that only unexpected failures stand out.
|
|
This commit also removes the extraneous "=>" token from Fail messages and
prevents them from losing all the formatting information.
|
|
|
|
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
|
|
unification fails due to that, during a conversion step.
|
