aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Fix #11941: anomaly in equality schemesGaëtan Gilbert
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
2020-03-01test-suite file for spurious universe generationMatthieu Sozeau
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
2020-02-26Consolidate int63-related notationsMaxime Dénès
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
2020-02-23Merge PR #11120: Refactoring code for application printing + fixing #11091 (i...Emilio Jesus Gallego Arias
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
2020-02-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
2020-02-22Merge PR #11639: Fixes #10917: anomaly in building return clause of n-ary pat...Emilio Jesus Gallego Arias
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence of...Pierre-Marie Pédrot
2020-02-09Merge PR #11518: Fix #11515: Ltac2 rewrite on wildcard.Gaëtan Gilbert
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-04Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
2020-01-08Close #11133Gaëtan Gilbert
2020-01-08Close #11168Gaëtan Gilbert
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-20Add test cases for #9490 and #9532Maxime Dénès
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ...Emilio Jesus Gallego Arias
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ...Pierre-Marie Pédrot
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-22Add test for #11161Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:25:38 +0000