aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2019-01-29Update update-compat.py scriptJason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost o...Gaëtan Gilbert
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-05Add test for #8951.Gaëtan Gilbert
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
2018-11-20Rename gh->bug_ test filesGaëtan Gilbert
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-13Merge PR #8886: [VM] Fix compilation of int31 eliminatorsMaxime Dénès
2018-11-13Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.Pierre-Marie Pédrot
2018-11-12Merge PR #8892: Fix part of #8224: grounding open term in fixpointsPierre-Marie Pédrot
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is br...Maxime Dénès
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
2018-11-02Fixing one instance of bug #8224 (grounding term w/o knowing if it has evars).Hugo Herbelin
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
2018-10-31[ssr] better doc for the IPatDispatch ASTEnrico Tassi
2018-10-31test-suite entry for issue #8544Cyril Cohen
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-23Fixing #8794 (anomaly with abbreviation involving both term and binders).Hugo Herbelin
2018-10-21Adding a regression test for bug #8785 (missing univ constraints registration).Hugo Herbelin
2018-10-19Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.Pierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-10[test-suite] rename a fileVincent Laporte
2018-10-10Merge PR #6218: Fix #5197, handling of algebraic universesPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-30 13:47:38 +0000