aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
2020-08-26Merge PR #12881: Deprecate intro_usingPierre-Marie Pédrot
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
2020-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
2020-08-25[test-suite] close the proofEnrico Tassi
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its documenta...Hugo Herbelin
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ...coqbot
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of...Pierre-Marie Pédrot
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to be...Pierre-Marie Pédrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-19Improve `make approve-output`Jason Gross
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the tes...Martin Bodin
2020-08-19No more arithmetic directory test-suite.Hugo Herbelin
2020-08-18Fix subject reduction VS cumulative inductives and function etaGaëtan Gilbert
2020-08-18Change OUnit package name to ounit2.Tanaka Akira
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
2020-08-18Tactic replace: adding support for registration of an equality in Type.Hugo Herbelin
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
2020-08-13Merge PR #12479: Bring Int63 notations into line with stdlibAnton Trunov
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[micromega] Fix bug#12790Frédéric Besson
2020-08-10[zify] fix for bug#12791Frédéric Besson
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Int63 notations into line with stdlibJason Gross
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-08-09Fixing a coercion entry transitivity bug.Hugo Herbelin
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Define...Pierre-Marie Pédrot
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:22:26 +0000