aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-02Understand Mangle Names in implicit generalizationGaëtan Gilbert
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-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-30Merge PR #13021: Almost fully moving funind to new proof enginePierre-Marie Pédrot
2020-09-30Merge PR #13032: More precise information when unification fails because of i...Pierre-Marie Pédrot
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
2020-09-29Applying ocamlformat.Hugo Herbelin
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-09-29Adding a few tacticals for the purpose of porting funind to new proof engine.Hugo Herbelin
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-09-29Merge PR #13101: Reduce nitpick_ignore list a little.Clément Pit-Claudel
2020-09-29Merge PR #13097: Modify how quotations handle whole sentences.coqbot-app[bot]
2020-09-29Merge PR #13039: Lint stdlib with -mangle-names #3coqbot-app[bot]
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-28Getting rid of temerarious EConstr.to_constr in Himsg.Hugo Herbelin
2020-09-28Merge PR #13105: [nix] CI script wrapper now requires Pythoncoqbot-app[bot]
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
2020-09-28More precise information when unification fails because of incompatible candi...Hugo Herbelin
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ...coqbot-app[bot]
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ...coqbot-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 #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...coqbot-app[bot]
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 06:14:15 +0000