| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Commit 84c2433a introduced the Any type alias as the Haskell extracted
version of MiniML's Tunknown. However, the code to define the Any
type alias was generated conditional on usf.magic. As it turns out,
sometimes Tunknown appears even if usf.magic is false (i.e., even if
MLmagic does not appear anywhere in the AST). This produced Haskell
code that would not compile; e.g.:
% coqtop
Coq < Extraction Language Haskell.
Coq < Extraction Library Datatypes.
The file Datatypes.hs has been created by extraction.
% ghc Datatypes.hs
[1 of 1] Compiling Datatypes ( Datatypes.hs, Datatypes.o )
Datatypes.hs:261:17: Not in scope: type constructor or class `Any'
Datatypes.hs:261:24: Not in scope: type constructor or class `Any'
The fix is straightforward: produce the code that defines the Any type
alias if usf.tunknown is true.
|
|
replacement for 8.4's "Require Omega").
|
|
`end proof` changes the proof mode to `"Classic"`.
|
|
So that the commands are assigned the appropriate status of syntax-changing or not, as well as the proof mode they are setting.
|
|
It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(Fix for bugs #3470 and #3694)
|
|
|
|
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.
|
|
After executing a command classified as VtProofStep the stm
prints the goals (if used via the tty API).
|
|
|
|
- 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
|
|
|
|
instances and forgeting about the evars and universes that could appear
there... dirty hack gone, using the evar map properly and avoiding
needless constructions/deconstructions of terms.
|
|
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
|
|
|
|
|
|
|
|
|
|
of plugins.
|
|
|
|
|
|
|
|
|
|
|
|
Of course such proofs cannot be processed asynchronously
|
|
|
|
typecheck with definitions and thread it accordingly when typechecking
module expressions.
|
|
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
|
|
|
|
|
|
|
|
|
The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.
|
|
Since name clashes are discovered by side effects, the order of traversal of
module structs cannot be changed.
|
|
|
|
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
|
|
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
|
|
|
|
