aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
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-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-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
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-29Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Pierre-Marie Pédrot
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
2018-03-27Fixing #5500 (missing test in return clause of match leading to anomaly).Hugo Herbelin
2018-03-26Fixes #7011 (Fix/CoFix were not considered in tactic unification).Hugo Herbelin
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Merge PR #6895: [compat] Remove "Refolding Reduction" option.Maxime Dénès
2018-03-08More examples about shelve/given_up in tactic-in-terms.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-08Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Maxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-02-24Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Maxime Dénès
2018-02-21Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 07:52:48 +0000