| Commit message (Collapse) | Author | Age |
|\ |
|
|\ \ |
|
| |\ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
| | | | | | | |
|
|/ / / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.
|
| |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
To handle dynamic printing in CoqIDE we listen to the
`size_allocate` signal , [see more details in
6885a398229918865378ea24f07d93d2bcdd2802]
However, we must be careful to protect against scrollbar creation: it
is possible for the `size_allocate` handler to change the size when
inserting text (due to scrollbars), thus we may enter in an infinite
loop.
Our fix is to check if the width has really changed, as done in
`Wg_MessageView`.
This fixes the problem noted by @herbelin in
https://coq.inria.fr/bugs/show_bug.cgi?id=5417
|
|/ / / / |
|
| | |/ |
|
|\ \ \ |
|
| | | | |
|
| |/ / |
|
|\ \ \ |
|
|\ \ \ \
| | |_|/
| |/| | |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \
| |_|_|_|_|_|_|/
|/| | | | | | | |
|
|\ \ \ \ \ \ \ \
| | |_|_|/ / / /
| |/| | | | | | |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | | |
|
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | |
| | | | | | | | | |
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.
|
|\| | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \
| | |_|_|/ / / / / /
| |/| | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
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 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
|
| | | | | | | | | | | |
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
There are now two field structures for R: one in RealField and one in
RIneq. The first one is used to prove that IZR is a morphism which is
needed to define the second one.
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
This prevents Coq from unfolding IZR in ring_simplify and field_simplify.
This is a change of behavior for users of morphism rings, so they might have
to pass the postprocess option to Add Ring/Field if they want morphisms to be
automatically expanded.
There are two predefined morphisms in the standard library: IDphi (when
polynomial coefficients have the same type as constants) and gen_phiZ (when
the only available constants are 0 and 1). They are hardcoded as transparent.
|
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | |
| | | | | | | | | | | |
There are two main issues. First, (-cst)%R is no longer syntactically
equal to (-(cst))%R (though they are still convertible). This breaks some
rewriting rules.
Second, the ring/field_simplify tactics did not know how to refold
real constants. This defect is no longer hidden by the pretty-printer,
which makes these tactics almost unusable on goals containing large
constants.
This commit also modifies the ring/field tactics so that real constant
reification is now constant time rather than linear.
Note that there is now a bit of code duplication between z_syntax and
r_syntax. This should be fixed once plugin interdependencies are supported.
Ideally the r_syntax plugin should just disappear by declaring IZR as a
coercion. Unfortunately the coercion mechanism is not powerful enough yet,
be it for parsing (need the ability for a scope to delegate constant
parsing to another scope) or printing (too many visible coercions left).
|
| | | | |_|_|/ / / /
| | | |/| | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.
Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
A bang indicates an argument that must be reduced, a star indicates an
argument that must be handled recursively.
PEeval: R r0 r1 add mul sub opp C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8! 9 10! 11 12* 13!
FEeval: R r0 r1 add mul sub opp div inv C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9 10! 11 12! 13 14* 15!
Pphi_dev: R r0 r1 add mul sub opp C c0 c1 ceq phi sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12! 13* 14!
Pphi_pow: R r0 r1 add mul sub opp C c0 c1 ceq phi Cpow powphi pow sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12 13! 14 15! 16* 17!
display_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13! 14* 15! 16!
display_pow_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi Cpow powphi pow sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13 14! 15 16! 17* 18! 19!
PCond: R r0 r1 add mul sub opp eq C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9! 10 11! 12 13* 14!
|
| | | | | | | | | | |
|