| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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).
|
|
|
|
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
|
|
modules."
This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
|
|
This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
|
|
This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda.
|
|
|
|
match predicates for vm_compute and compile polymorphic definitions
to constant code. Add univscompute test-suite file testing VM
computations in presence of polymorphic universes.
|
|
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
|
This is useful for PIDE based interfaces, since they can
build hyperlinks out of .glob files and let the
user jump to the corresponding .v files
|
|
Not supposed to be part of 8.5beta.
This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
|
|
|
|
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
|
|
|
|
|
respect dependencies between typeclass goals, trying to solve the least
dependent ones first.
|
