aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
2020-08-31Use a faster algorithm to check for class existence.Pierre-Marie Pédrot
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-08-30Merge PR #12952: Fix rendering of -> in micromegacoqbot-app[bot]
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-30Merge PR #12934: Enrich `evar_map` printer with future goals stackPierre-Marie Pédrot
2020-08-29Merge PR #12929: Make abstract compatible with mangle namesPierre-Marie Pédrot
2020-08-29Merge PR #12939: Fix configure check for zarithcoqbot-app[bot]
2020-08-29Fix configure check for zarithGaëtan Gilbert
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
2020-08-28Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor of...coqbot-app[bot]
2020-08-28Merge PR #12933: Add test for past anomalyPierre-Marie Pédrot
2020-08-28Merge PR #12932: par: print relevant subgoal when failingcoqbot-app[bot]
2020-08-28Drop opaque bodies of abstracted definitions.Pierre-Marie Pédrot
2020-08-28Enrich `evar_map` printer with future goals stackMaxime Dénès
2020-08-28Name saved goals in name_mangling testGaëtan Gilbert
2020-08-28Clarify variable names in abstract implementationGaëtan Gilbert
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
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-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-28Merge PR #12924: Remove meta-based refiner code in ssrcoqbot-app[bot]
2020-08-28Merge PR #12632: [state] A few nits after consolidation of state.coqbot-app[bot]
2020-08-27[zarith] ChangelogEmilio Jesus Gallego Arias
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numtok] [zarith] SimplificationsEmilio Jesus Gallego Arias
2020-08-27[zarith] [notation] Build less intermediate valuesEmilio Jesus Gallego Arias
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-27[state] A few nits after consolidation of state.Emilio Jesus Gallego Arias
2020-08-27Remove the now unused Evarutil.mk_new_meta function.Pierre-Marie Pédrot
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-27Merge PR #12922: Fix .gitignore after the merge of #12849.coqbot-app[bot]
2020-08-27Fix .gitignore after the merge of #12849.Pierre-Marie Pédrot
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
2020-08-27Merge PR #12918: tacinterp mini cleanup useless letinPierre-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 #12850: Avoid running configure when plugins/ modifiedcoqbot-app[bot]
2020-08-27Merge PR #12877: Propagate in-context information for explicitation of extra ...coqbot-app[bot]
2020-08-27Merge PR #12867: Fast freeze summarycoqbot-app[bot]
2020-08-27Merge PR #12911: Use the lite variants of performance tests in the bench defa...coqbot-app[bot]