| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
implicit is found whether one writes (sig P) or {x|P x}.
|
|
implicit arguments when in beautification mode.
|
|
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
does not print to ** which is a keyword.
|
|
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
|
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _",
the same way as if we had said:
Arguments eq_refl {A} {x}.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
What one needs to know in 3rd party makefiles, like plugins ones,
is the Coq version and the OCaml version number. This option prints
the 2 values on a single line separated by spaces. The already existing
--version outputs the same piece of info but in a format meant for user
consumption, and hence harder to parse.
|
|
Used to be an `exit 1`, now an error message is printed on stderr.
This helps people experimenting with the XML protocol.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Introduced by b21fefc0ec0aab2560d0b654f1a1f4203898388b
|
|
This is a stupid fix that only allows to take into account the change in
memory layout. The check will simply fail when encountering a unguarded
inductive or (co)fixpoint.
|
|
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
|
|
|
|
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
|
Following CeCILL-B 5.3.2, we are allowed to redistribute the
software under the same license of Coq as long as we credit.
|
|
|
|
|
|
|
|
|
|
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
|
