aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-09-11Merge PR #13005: Add simple-io to dev/ci/nix.Vincent Laporte
2020-09-10Merge PR #13001: Update INSTALL.mdcoqbot-app[bot]
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
2020-09-10Fix typos.Théo Zimmermann
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-09-10Add simple-io to dev/ci/nix.Théo Zimmermann
2020-09-10Merge PR #12997: Add a fast-path to Tactics.e_change_in_hyps.Hugo Herbelin
2020-09-10Merge PR #12998: changelog entry for 12857coqbot-app[bot]
2020-09-10Add a fast-path to Tactics.e_change_in_hyps.Pierre-Marie Pédrot
2020-09-10Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rstEnrico Tassi
2020-09-09Update INSTALL.mdMatthieu Sozeau
2020-09-09Merge PR #12994: Fix docgram's dune file following #12085.coqbot-app[bot]
2020-09-09dune: pass -bin-annot to configureGaëtan Gilbert
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
2020-09-09changelog entry for 12857Enrico Tassi
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-09Merge PR #12905: Lint stdlib with -mangle-names #2coqbot-app[bot]
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Fix docgram's dune file following #12085.Théo Zimmermann
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-08Merge PR #12991: [Small typo] Update match.rstcoqbot-app[bot]
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
2020-09-08[Small typo] Update match.rstClément Blaudeau
2020-09-08Merge PR #12927: Explain that tactics applied to multiple goals don't preserv...coqbot-app[bot]
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...Pierre-Marie Pédrot
2020-09-08Merge PR #12987: Fix printing of `change` tacticPierre-Marie Pédrot
2020-09-07Circumvent revealed bug of evar resolution for fixpointMaxime Dénès
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-07Merge PR #12988: Remove dead code in clenv-generating functions.Hugo Herbelin
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-09-07Remove dead code in clenv-generating functions.Pierre-Marie Pédrot
2020-09-07Add changelog entryEdward Wang
2020-09-07Add iff variants for other list lemmasEdward Wang
2020-09-07Add iff variant for app_inj_tailEdward Wang
2020-09-06Fix printing of `change` tactic, which was printed as `change_no_check` and v...Lasse Blaauwbroek
2020-09-06Merge PR #12976: Remove clenv chaining in EqualityHugo Herbelin
2020-09-06Merge PR #12980: Simplify the implementation of ElimHugo Herbelin
2020-09-04Remove a unused function from the Clenv API.Pierre-Marie Pédrot
2020-09-04Remove the last use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-04Inline the last use of apply_on_clause in Equality.Pierre-Marie Pédrot
2020-09-04Remove a useless use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-04Merge PR #12969: CI: build Iris examples instead of lambda-Rustcoqbot-app[bot]
2020-09-04Statically enforce that elim is passed a fully applied inductive type.Pierre-Marie Pédrot
2020-09-04Restrict a spurious call to a reduction to a quantified inductive type.Pierre-Marie Pédrot
2020-09-04Defunctionalize the mk_elim creation in Elim.Pierre-Marie Pédrot
2020-09-04Enforce the argument of elim functions to be a variable.Pierre-Marie Pédrot
2020-09-04Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unif...coqbot-app[bot]
2020-09-04Merge PR #12900: [bench] Also upload the raw timing files, etcPierre-Marie Pédrot
2020-09-04Merge PR #12912: Fix algebraic comparison with sprop on one sidePierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-14 22:29:22 +0000