| Age | Commit message (Collapse) | Author |
|---|
|
Previously a union type was used for externing.
In particular, moving extended_glob_local_binder to glob_constr.ml.
|
|
RawLocal -> CLocal
|
|
This is a bit long, but it is to keep a symmetry with constr_expr.
|
|
|
|
No more constr_expr in it.
|
|
|
|
Aligned the type binder_data to the naming scheme used in (raw)
local_binder and Rel.Declaration.t. Made some code factorization.
Still to do: align type Glob_term.glob_binder to the Assum/Def format
too.
Note: this includes fix of anomaly with 'pat in cofix (dec77f282).
|
|
|
|
Instead of crawling the whole undefined evar map, we use the fold_right
function to process evars in decreasing order.
|
|
|
|
|
|
|
|
|
|
|
|
And an extra minor changes (use of zeroone when relevant, use of type
rather than term).
|
|
|
|
|
|
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
|
|
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
|
|
|
|
|
|
Need to check inside control expressions. Also fixes handling of
[Redirect "file" Defined.] and [Timeout n Defined.].
Fixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411):
coqc -quick hangs on [Time Defined.]
|
|
|
|
|
|
|
|
|
|
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
|
|
We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
|
|
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
|
|
|
|
|
|
|
This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.
|
|
|
|
|
|
A lot of tactic calls actually use the open_constr_no_classes_flags option
which does not require checking anything about frozen evars. Computing it
upfront is useless in this case.
|
|
Most of the time, undefined evars are not modified by the considered function,
which leads to the costly recomputation of a trivial partition of evars. We
simply take advantage of physical equality to discriminate when this is
useless and special-case it in the type of frozen evars.
|
|
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
|
|
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
|
This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
|
|
|
|
This makes sense for clients willing to link to richpp.
|
|
|
|
|
|
|
|
|
|
This patch restores the proper printing of anomalies in coqtop / coqc
/ coqide. Currently, they are printed with an `Error` header, whereas
they should be printed with an `Anomaly" header.
This reopens an unfinished debate started in #390 , about how to
properly do "message" headers. Prior to #390, headers were handled
inconsistently, sometimes, `Error` or `Anomaly` were added in
`CErrors`, which lives below of the tagging system, thus some times we
got no coloring (c.f. https://coq.inria.fr/bugs/show_bug.cgi?id=4789),
but some other times the headers were added by the message handlers in
Feedback.
PR #390 takes the position of identifying the messages with the
`Feedback.level` tag, and letting the backends to the tagging. This
makes sense as the backends may want to interpret the "headers" in any
way they'd like. For instance, instead of printing: `Error: foo` they
may want to insert an image.
Note that this implies that CoqIDE doesn't currently insert an error
header on the first error case. This could be easily solved, but for
anomalies we could do in any of the ways explained below.
There are thus two natural ways to handle anomalies here: One is to
tag them as errors, but add a text header, this is done now, with the
small optimization in the case the handled has access to the exception
itself. The second way is to add a new `Feedback.level` category and
tag the anomalies appropriately. We would need also to modify Fail in
this case, or to completely remove it from the protocol.
I guess feedback from the rest of developers is needed before
committing to a strategy, for now this patch should be good.
|
|
This adds at least support for camlp5 6.14 (in addition to 6.17).
|
|
We need to do a bit of hacking, but it should be fine for the short
term.
c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
|
|
|
