| Age | Commit message (Collapse) | Author |
|---|
|
Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.
|
|
|
|
I've included some other changes that didn't happen in this PR.
|
|
The ErrorMsg datatype was introduced to allow locations in messages,
however, it was redundant with error and used only in one place.
We remove it in favor of a more uniform treatment of messages with
location. This patch also removes the use of `Loc.ghost` in one place.
Lightly tested.
|
|
The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.
Next step is to remove redundant MsgError feedback type.
|
|
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
|
IMO level indicators are not the proper place to store this information.
|
|
|
|
They were spotted by profiling tactics manipulating huge terms, provided by
Jason Gross.
|
|
Use a much dumber algorithm to recognize the shape of equalities.
|
|
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
|
|
|
Do not evar-normalize the argument provided by afterHyp.
|
|
We do not allocate a closure in the main loop, and do so only when needed.
|
|
We do not check for presence of a variable in a global definition when we know
that this variable was not present in the section.
|
|
Do not normalize all goals beforehand.
|
|
Do not evar-normalize the term to substitute with. The engine should be
insensitive to this kind of modification.
|
|
We use simple variable substitution instead of full-power term
matching.
|
|
|
|
|
|
|
|
|
|
|
|
Now that the plugins are packed, a plugin forms now a unique
compilation unit, and we only need to install the main cmi file of
this plugin (foo_plugin.cmi).
Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and
some other cleanup in Makefile.common (no more INITPLUGINS variable,
for instance).
|
|
We do not recompute shortest name identifier for global references that were
already traversed. Furthermore, we share the computation of identifiers
between invokations of the name generating function.
This drastically speeds up detyping for huge goals, further mitigating the
shortcomings of the fix for bug #4777.
|
|
Now, only 'phony' targets could be declared just via dependencies.
For 'real-file' targets such as doc/refman/html/index.html, there
should be a concrete production rule.
|
|
|
|
It seems like this code was copy-pasted from kernel/inductive.ml. It was
already dubious enough in the kernel. It feels completely wrong in the
checker.
|
|
As reported by PMP, this was not yet the case. The culprit
was the build of coqdep_boot by a one-liner ocamlopt taking all
the necessary .ml files as arguments (in the right order). This
was nice and short, and correct wrt dependencies, but had the
inconvenient of building some .cmi *after* their corresponding
.cmx, while the rest of the Makefile relies on the reverse order
(see the section about MLWITHOUTMLI). Hence on the next run,
make was thinking that these .cmx weren't up-to-date.
For solving this issue, we now build coqdep_boot (and other tools)
via a list of .cmx and let our infractructure build them (after
their .cmi). The only drawback is the 6 extra lines to hardcode
the dependencies of the *.cm(o|i|x) needed for coqdep_boot.
(since the .ml.d aren't already taken in account by make at that
time).
|
|
|
|
|
|
|
|
with recent Coq
|
|
Coq locations already had support for this, but were containing dummy
information. We now don't need anymore to reconstruct this information by
browsing the file when printing an error message or enriching exceptions on the
fly.
It also became easier to interface with Coq since locations emitted by the
lexer now always contain full information.
On the API side, Loc.represent disappeared and Loc.t is now exposed as record.
It is less error-prone than manipulating a tuple of 5 integers. Also,
Loc.create takes 5 arguments instead of 3 and a pair.
|
|
using a custom feedback message in response to "Show Ltac Profile."
|
|
|
|
We do not check that an hypothesis is used in context declarations that
occur before it.
|
|
above it.
|
|
|
|
|
|
This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
|
|
|
|
|
|
|
|
This fixes bug #4828 (https://coq.inria.fr/bugs/show_bug.cgi?id=4828).
|
|
|
|
I had to remove code handling the -type-in-type option introduced by commit
9c732a5. We should fix it at some point, but I am not sure that using the
checker with a system known to be blatantly inconsistent makes much sense
anyway.
|
|
|
|
|
|
|
