aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
2020-08-25Merge PR #12758: Fixing a coercion entry transitivity bug.coqbot-app[bot]
2020-08-25[test-suite] close the proofEnrico Tassi
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-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-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
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qua...Théo Zimmermann
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive decl...Pierre-Marie Pédrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ...Emilio Jesus Gallego Arias
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when a...Gaëtan Gilbert
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ar...Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:28:35 +0000