| Age | Commit message (Collapse) | Author |
|---|
|
|
|
for uniformity with other Debug options.
|
|
|
|
Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends
already on all the .cmx inside it, no need to state explicitely
that the .cmxs depends on these inner .cmx. Same thing concerning
.cmxs built out of a single .cmx.
|
|
Earlier (as in #4812), a target with some declared dependencies (e.g.
in a .d) but no building rule would lead to a successful build,
even though it is actually incomplete.
Side effect: it is now mandatory to declare phony targets in a
.PHONY statement.
|
|
|
|
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
|
|
In pre 8.6, `Pp` provided its own reimplementation of
`Pervasives.flush_all`, with different semantics.
Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of
points were silently switched to the `Pervasives` version, which may
lead to some subtle printing differences.
As a preventive measure, we restore the same semantics for these parts
of the codebase.
Note that we don't re-introduce Coq's `flush_all` for several reasons:
- Consumers of the logging API should not mess with flushing and
Formatters as this is backend dependent (i.e: when in IDEs).
Use of `Format` should be fully encapsulated if we want some hope of
IDEs taking full control.
- As used, the old semantics of `flush_all` were fragile.
|
|
We revert the change of flushing strategy in the toplevel.
PR #179 introduced a different flushing in toplevel, but it creates
problems as new lines appear when Set Printing Width is large and proof
general complains, see bugzilla#4784. The use of `flush_all` also
produces missing output.
IMO, this is a pitfall of the current setup, in particular, `Format` is
used without enclosing expressions in top-level boxes, as required. This
results in undefined behavior and fragile printing such as this bug
exemplifies.
Test suite passes.
|
|
Restore the .cmxa-->.cmxs rule from the Makefile. Sorry, I was thinking
that all plugins would now be built from .mlpack (hence using only the
.cmx-->.cmxs rule), and I forgot about this coqidetop business.
Now the really intersting question is : why on earth 'make world' was
silently failing to build this file but succeeding nonetheless ?!
|
|
We export `Cerrors.EvaluatedError` so plugins and STM consumers can
catch it.
It took me a while to make my mind on this one, but now I am convinced
this is the right thing to do. (Another possibility is to remove
`EvaluatedError` altogether).
The rationale is as follows: when using `Stm.{add,observe}` it
will be frequent for Coq to raise a public-facing exception, however the
toplevel will wrap it into the `EvaluatedError`.
Thus, we get exceptions that we are supposed to handle, but its wrapping
in `EvaluatedError` prevents us from a more meaningful exception
handling: we are stuck with calling the printer.
In particular, this allows SerAPI/jsCoq to provide proper serialization
of most public exceptions.
|
|
|
|
|
|
Conflicts:
Makefile.common
|
|
|
|
Add -o option to coqc
|
|
|
|
Documentation also updated.
|
|
|
|
|
|
|
|
|
|
|
|
This is the "error resiliency" mode for STM
|
|
They can still be used at the toplevel.
|
|
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals
numbered 1 and 3 to 5.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8.
|
|
This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
declared inside sections, when all the section's
variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
which are not parameterized by polymorphic universes/assumptions.
Add fix for part 1 of bug #4816
|
|
|
|
|
|
Check that the polymorphic status of everything that
is parameterized in nested sections is coherent.
|
|
|
|
|
