| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The Arguments command tends to emit the following warning even when
properly used:
This command is just asserting the number and names of arguments of cons.
If this is what you want add ': assert' to silence the warning. If you
want to clear implicit arguments add ': clear implicits'. If you want to
clear notation scopes add ': clear scopes'
In fact, even ': assert' does not silence it, contrarily to what the message
suggests.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Now that ML tactics are not dispatched according to the type of their arguments
anymore, one has to take care of the way potentially atomic tactics are handled.
This patch ensures that the atomic tactics generated by the TACTIC EXTEND
macro have the right length and the right order.
There may be very rare trouble if two ML tactics in the same entry are of the
form
"foo" x1 ... xn
"foo" y1 ... ym
where all xi and yi may be empty. I doubt that the legacy implementation
behaved well in this case anyway.
|
|
A non empty dir detected as an empty one.
|
|
A non empty dir detected as an empty one.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.
|
|
|
|
Structures. Text mode + a "Require Import" in a module which provokes
suspect warnings "Exception Not_found".
|
|
a line on "Intuition Negation Unfolding".
|
|
Argument" which I used temporarily in a branch to have "destruct eq_dec"
working like in v8.4 and not like the "destruct (eq_dec _ _)"
of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like
"destruct eq_dec" was working in 8.4 (and is still working in 8.5).
|
|
Set Printing Existential Instances (see bug report #3951).
|
|
obviously inconsistent with the decisions taken in commits
2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606.
Now having options Boolean Equality Schemes and Decidable Equality Schemes.
|
|
|
|
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
|
Furthermore, ML tactic dispatch is not done according to the
type of its argument anymore.
|
|
Since name clashes are discovered by side effects, the order of traversal of
module structs cannot be changed.
|
|
|
|
|
|
|
|
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
|
|
|
|
match the overall style.
|
|
It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.
|
|
part.
|
|
|
|
|
|
Fixes #3939.
|
|
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
|
|
|
|
Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.
The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.
|
|
Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.
The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.
|
|
actually calling the VM at Qed time.
|
|
|
|
Follow-up on Matthieu's d030ce0721.
|
|
|
|
|
|
printing functions touched in the kernel).
|
