| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
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 ?!
|
|
Add -o option to coqc
|
|
|
|
Documentation also updated.
|
|
|
|
|
|
|
|
This is the "error resiliency" mode for STM
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
|
|
non-recursive notations (#4815).
|
|
|
|
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
|
|
The tentative fix in f9695eb4b (which I was afraid it might be too
strong, since it was implying failing more often) indeed broke other
things (see #4813).
|
|
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
|
This can happen with the "with" clause (see e.g. #4782), but also with
recursive calls in first-order unification (e.g. "?n a a b = f a" when
a matching between "b" and "a" is tried before expanding f).
|
|
|
|
Trying to now catch all unification errors, but without a clear view
at whether some errors could be tolerated at the point of checking the
type of the binding.
|
|
Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
|
|
|
|
|
|
|
|
|
|
complexity comes before tests in O(n) complexity.
|
|
|
|
|
|
|
|
|
|
Typically, a problem of the form "?x args = match ?y with ... end" was
a failure even if miller-unification was applicable.
|
|
|
|
Renouncing to bypass the library path given by "camlp5o -where" what
we assume to be the default library location, considering that
-usecamlp5dir is here to deal with the non-standard installation
layout.
Renouncing to find camlp5 libraries in a subdirectory of the ocaml
library directory since we now know that camlp5o is found and that we
have a priori to trust option -where of camlp5o.
Additionally falling back on looking for camlp4 if a camlp5 library is
found but no camlp5 binary. Also using camlp5o as a reference since
after all this is camlp5o that we need.
In particular, this fixes situations where -usecamlp5dir is given but
"camlp5o -where" contradicts it.
If something has to be checked on windows, please tell.
|
