| Age | Commit message (Collapse) | Author |
|---|
|
it was failing with Not_found before previous commit). This "fixes"
the loop by expanding local defs in "imitate" rather than keeping them
explicit. The example is otherwise too large for me to be able to
understand where does the loop come from.
|
|
- Remove dead code in evarconv.
|
|
|
|
|
|
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
|
|
while Context gives different type to each variable, this test-suite file shows this.
|
|
|
|
- Move HoTT bug #30 to closed
|
|
of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
|
|
using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
|
|
name of replaced hypothesis.
|
|
|
|
|
|
|
|
|
|
I'd add more, but I'm tired and it's late and I should sleep. Maybe
I'll pick up at 3279 (working down) another day.
Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly. So there's no way I can think of to
test it. I've left it in the [opened] directory anyway.
|
|
|
|
|
|
I've marked new failing commands that I'm confused about with "???"; I'm
not sure whether or not they should fail there, but we should keep the
test-suite compiling, probably.
|
|
declare takes care of ignoring side effects that are available in the
global environment. This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof. In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.
Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
the constant is already there (it can be there, no need to regenerate it
but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
really needed to be inlined.
bottom line: STOP using abstract.
|
|
|
|
|
|
|
|
|
|
|
|
The contract is that a file in bugs/opened should not raise errors if
the bug is still open.
Some of them fail for different reasons than they used to; I'm not sure
what to do about these.
|
|
|
|
hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently fails.
I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
|
|
fixing two opened bugs from HoTT/coq.
|
|
into JasonGross-working-polyproj-tests
|
|
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
|
|
|
|
|
|
These regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently passes.
I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
|
|
polymorphic (fixes bug #3043).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also allow [projT1]/[projT2] to work for [sigT2]s and
[proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions.
This closes Bug 3044.
This closes Pull Request #4.
|
|
Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
|
|
Closed in 69c4d0fd7b8325187e8da697a9c283594047d.
I used [Timeout 2] to distinguish between stack overflow and immediate
return.
|
|
Closed in f65fa9de8a4c9c12d933188a755b51508bd51921
I used [Timeout 2 Fail] to test the difference between immediate failure
and stack overflow. Hopefully this is robust enough.
|
|
It was fixed in c3feef4ed5dec126f1144dec91eee9c0f0522a94.
The test case uses [Timeout 2] to test for "Coq runs instantaneously
rather than running out of memory". Hopefully this is robust enough.
|
