aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)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
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
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
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
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
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Matthieu Sozeau
2018-06-14Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Matthieu Sozeau
2018-06-12Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Hugo Herbelin
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
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-06-05Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...Maxime Dénès
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
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 pattern-matc...Matthieu Sozeau
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 ta...Matthieu Sozeau
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
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
2018-05-20Add test cases from #7554Tej Chajed
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 s...Gaëtan Gilbert
2018-05-13Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoRalf Jung
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
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...Jason Gross
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
2018-04-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 15:02:46 +0000