aboutsummaryrefslogtreecommitdiff
path: root/test-suite
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-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
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-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
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-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-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-21Make print-pretty-timed robust against non-output-sync logsJason Gross
2020-09-18[lib] make canonical_path_name always absolute (fix #13031)Enrico Tassi
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo 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-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...Pierre-Marie Pédrot
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-04Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unif...coqbot-app[bot]
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
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-31Fix mangle names issue in inductionGaëtan Gilbert
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 07:58:37 +0000