aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12605: [test-suite] async-proofs off in tests with Fail TimeoutGaëtan Gilbert
2020-06-30Merge PR #11977: Generate default names for bound universes of polymorphic de...Emilio Jesus Gallego Arias
2020-06-29[test-suite] async-proofs off in tests with Fail TimeoutEnrico Tassi
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Merge PR #12530: Fix glob_sort_family for SPropMaxime Dénès
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-22Merge PR #12434: Slight improvement in naming dependent existential variables...Gaëtan Gilbert
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17Merge PR #12508: Fix #12507 Anomaly when using a ssreflect `reflect` viewCyril Cohen
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
2020-06-16make the linter happyEnrico Tassi
2020-06-15[ssr] fix env handling in error message (fix #12507)Enrico Tassi
2020-06-14fix according to review by @pi8027Frédéric Besson
2020-06-11[test-suite] [stm] Interactive test case for fail-on-qed.Emilio Jesus Gallego Arias
2020-06-11Merge PR #12443: Fix #12442: Confusing error message when the intro pattern o...Pierre-Marie Pédrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n t...Vincent Semeria
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-01Slight improvement in naming existential variables.Hugo Herbelin
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async m...Emilio Jesus Gallego Arias
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-25Fix output tests for location errors when running in async mode.Théo Zimmermann
2020-05-22[coqchk] Add testPierre Roux
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-21Fix an uncaught python exception in timingJason Gross
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
2020-05-21Merge PR #12358: [topfmt] Set formatter + flush fixGaëtan Gilbert
2020-05-20Print a newline at the end of timing tablesJason Gross
2020-05-20Merge PR #12350: [test-suite] Ensure copies of files are writableGaëtan Gilbert
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:01:23 +0000