aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
2020-08-29Merge PR #12929: Make abstract compatible with mangle namesPierre-Marie Pédrot
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
2020-08-28Merge PR #12933: Add test for past anomalyPierre-Marie Pédrot
2020-08-28Name saved goals in name_mangling testGaëtan Gilbert
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
2020-08-28About: Add a mention that arguments have been renamed, if ever it is the case.Hugo Herbelin
2020-08-28Where there are several lists of implicit arguments, don't pretend names matter.Hugo Herbelin
2020-08-28Do not write "rename" for arguments in About, since these arguments are valid...Hugo Herbelin
2020-08-28When printing the type in About, use the renamed arguments.Hugo Herbelin
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-28In "About", print all arguments, even if it is trailing list of _.Hugo Herbelin
2020-08-28Add test for past anomalyGaëtan Gilbert
2020-08-28par: print relevant subgoal when failingGaëtan Gilbert
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
2020-08-27Merge PR #12499: Clean future goalsPierre-Marie Pédrot
2020-08-27Merge PR #12913: Modify lia to work with -mangle-namescoqbot-app[bot]
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ...coqbot-app[bot]
2020-08-26Modify lia to work with -mangle-namesJasper Hugunin
2020-08-26Add test for #10939Maxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:32:34 +0000