| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
(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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
In the case of an inner module without explicit signature,
(and not used later in a functor application), we now extract
only the needed items (used later or asked by the user),
instead of blindly extracting all fields as earlier.
|
|
Since type variables are local to the definition, we simply rename
them in case of unicode chars. We also get rid of any ' to avoid
Ocaml illegal 'a' type var (clash with char litteral).
|
|
|
|
- Common.get_native_char instead of just a pp function of this char
- Enrich the record projection table
|
|
|
|
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.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
right-hand side of a "change with": the rhs lives in the toplevel
environment.
|
|
for Functional Induction was failing because of minus now an alias).
Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):
"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.
"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
|
|
|
|
|
|
This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
|
|
|
