aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
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
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound varia...Matthieu Sozeau
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-09-06Fixing #8270 (cbn was calling zeta even when not asked for).Hugo Herbelin
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-05Merge PR #7968: Restrict universes in comInductiveGaëtan Gilbert
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 04:18:09 +0000