aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...Pierre-Marie Pédrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-11Fix #7812Attila Gáspár
2020-04-03Fix the test for bug #4544.Pierre-Marie Pédrot
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 11:26:58 +0000