aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-09-03Merge PR #12876: Namegen.visible_ids: fixing what seems to be typosPierre-Marie Pédrot
2020-09-03Merge PR #12973: Random cleanup around the data structures used in EqualityHugo Herbelin
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
2020-09-02Merge PR #12943: Move Elim-specific codeHugo Herbelin
2020-09-02Remove the opening of CErrors in Elim.Pierre-Marie Pédrot
2020-09-02Code deduplication in Elim.Pierre-Marie Pédrot
2020-09-02Factorize the only uses of internal API in Elim for Inv.Pierre-Marie Pédrot
2020-09-02Make the Elim.branch_args type opaque.Pierre-Marie Pédrot
2020-09-02Further remove the type Elim.branch_assumptions.Pierre-Marie Pédrot
2020-09-02Remove unused API from Elim.Pierre-Marie Pédrot
2020-09-02Document the Equality.equality type in the ML file.Pierre-Marie Pédrot
2020-09-02Remove redundant data from the equality eliminator datatype.Pierre-Marie Pédrot
2020-09-02Do not look for a quantified inductive type in intropattern injection.Pierre-Marie Pédrot
2020-09-02Use a dedicated type for equality elimination.Pierre-Marie Pédrot
2020-09-02Merge PR #12883: Use a faster algorithm to check for class existence.coqbot-app[bot]
2020-09-01Merge PR #12872: Unify the shelvesPierre-Marie Pédrot
2020-09-01Unify the shelvesMaxime Dénès
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
2020-09-01Merge PR #12961: [declare] Return both declared constants in Derive path.coqbot-app[bot]
2020-09-01Merge PR #12962: Add zarith to the include path for ocamldebug-coqcoqbot-app[bot]
2020-08-31Add zarith to the include path for ocamldebug-coqJasper Hugunin
2020-08-31[declare] Return both declared constants in Derive path.Emilio Jesus Gallego Arias
2020-08-31Merge PR #12958: Fix load_printers after zarithcoqbot-app[bot]
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
2020-08-31Merge PR #12935: Drop opaque bodies of abstracted definitions.coqbot-app[bot]
2020-08-31Fix load_printers after zarithGaëtan Gilbert
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 08:14:23 +0000