aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
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
2018-10-09[test-suite] ensure file names are valid module namesVincent Laporte
2018-10-09Simplify code for [Definition := Eval ...]Gaëtan Gilbert
2018-10-09Fix nativenorm when an evar is in the wrong place.Gaëtan Gilbert
2018-10-08Fixes #8672 (ill-formed pattern substitution in notation with "let").Hugo Herbelin
2018-10-08Fix #5197, handling of algebraic universesMatthieu Sozeau
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-10-02Update the -compat flagsJason Gross
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-28Merge PR #8479: Fix #8478: Undeclared universe anomaly with sectionsPierre-Marie Pédrot
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting ev...Pierre-Marie Pédrot
2018-09-25Fixing #8532 (regression in Print Assumptions within a functor).Hugo Herbelin
2018-09-25Remove romegaVincent Laporte
2018-09-24Fixes #8215 ("critical" bug of type inference in interpreting evars by names).Hugo Herbelin
2018-09-21Merge PR #8455: Move tests in bugs/ to bugs/closed/.Théo Zimmermann
2018-09-19Move tests in bugs/ to the bugs/closed/.Nick Lewycky
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 19:11:33 +0000