aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-06Add test for #8004.Gaëtan Gilbert
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
We fix the issue by removing terms of the substitutions which have free variables and are thus not interpretable in the context of the "ltac:" subterm. This remains rather ad hoc, since, in an expression "Notation f x := ltac:(foo)", we interpret "x" at calling time of "foo" rather than at use time of "x" in foo, even if "x" is not necessary. We could also imagine that binders in the ltac expressions are then interpreted but that would start to be (very) complicated. Note that this will presumably "fix" ltac2 quotations at the same time.
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Matthieu Sozeau
subtyping.
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
It seems that lifting a term with a negative index is not equivalent to strengthening it by applying to a dummy substitution. This looks suspicious at best.
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Matthieu Sozeau
to anomaly)
2018-06-14Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵Matthieu Sozeau
in unification
2018-06-12Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Hugo Herbelin
This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using [].
2018-06-12Fixes #7780 (missing lift in expanding alias under a binder in unification).Hugo Herbelin
2018-06-10Fixing #7700 (section variables bound to abbreviations were not found).Hugo Herbelin
Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned.
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
Fix #5012.
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
2018-06-05Merge PR #7077: Preserving canonical structure of return predicate in ↵Maxime Dénès
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
2018-06-04Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Hugo Herbelin
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵Matthieu Sozeau
pattern-matching names
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
2018-06-04Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyMatthieu Sozeau
2018-06-04Merge PR #7189: Fix #5539: algebraic universe produced by cases.Matthieu Sozeau
2018-06-04Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵Matthieu Sozeau
tactic unification.
2018-06-04Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Matthieu Sozeau
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-05-30Fix #7113: Program Let Fixpoint in section causes anomalyGaëtan Gilbert
2018-05-29Fix #6951: Unexpected error during scheme creation.Pierre-Marie Pédrot
When creating a scheme for bifinite inductive types, we do not create a fixpoint.
2018-05-29Add test for #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-23Fix #7586: Anomaly "Uncaught exception Not_found".Pierre-Marie Pédrot
The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal.
2018-05-20Add test cases from #7554Tej Chajed
Failed in v8.7.2 but were fixed by v8.8.0.
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gaëtan Gilbert
symlink from repo
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
Fixes #7065
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵Jason Gross
removing the test.
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix.
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
We also make the code of [compact] in kernel/univ.ml a bit clearer.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:35:05 +0000