| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
being transparent
|
|
Off by default as it can be backwards-incompatible (e.g. produces
loop in the library without an additional Typeclasses Opaque directive
in RelationPairs).
|
|
|
|
non-universe-polymorphic
ID, fixing the script results in 3 universes for the stdlib again.
|
|
|
|
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
|
|
etc. (source of incompatibility).
|
|
etc. (source of incompatibility).
|
|
|
|
|
