aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a speci...coqbot-app[bot]
2020-10-06Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.Hugo Herbelin
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotatio...Pierre-Marie Pédrot
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...coqbot-app[bot]
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
2020-09-15A temporary fix of #13018 and #12775 for branch 8.2.Hugo Herbelin
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-09-03Fix incorrect debruijn handling when Record calls maybe_unify_params_inGaëtan Gilbert
2020-09-02Fixes #9403 and #10803 (missing flattening of nested applications in notations).Hugo Herbelin
2020-09-02Fixes part 1 of #12908 (collision involving a lonely notation).Hugo Herbelin
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
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-28par: print relevant subgoal when failingGaëtan Gilbert
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ...coqbot-app[bot]
2020-08-25Merge PR #12897: [test-suite] close the proof added in #12857coqbot-app[bot]
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-25[test-suite] close the proofEnrico Tassi
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo 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-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-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-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
2020-08-09Fixing a coercion entry transitivity bug.Hugo Herbelin
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-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
2020-07-08Adding test for #12525 (Search of lemmas in Include failing when in Module).Hugo Herbelin
2020-07-01UIP in SPropGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:17:45 +0000