aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-06Simplify Implicit_quantifiers.combine_params a bitGaëtan Gilbert
2020-10-06First list in cl_context is just booleansGaëtan Gilbert
2020-10-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
2020-10-05Change log for #12768.Hugo Herbelin
2020-10-05Adapting theories to unused pattern-matching variable warning.Hugo Herbelin
2020-10-05Wish #12762: warning on duplicated catch-all pattern with unused named variable.Hugo Herbelin
2020-10-05Document the removal of forward class hints.Théo Zimmermann
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-03Avoid magic numbersJim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
2020-10-02More details in the documentation of native arraysVincent Semeria
2020-10-02setoid_rewrite: record generated name when rewriting under lambdaGaëtan Gilbert
2020-10-02Understand Mangle Names in implicit generalizationGaëtan Gilbert
2020-10-02Cleanup rewrite.mlGaëtan Gilbert
2020-10-02Merge PR #13054: {new,setoid_}ring -> ringcoqbot-app[bot]
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
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-30Fix retyping anomaly in rewriteGaëtan Gilbert
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-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
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-28Put type-in-type flag in ugraph.Gaëtan Gilbert
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-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-28Remove the linter ocamlformat pass.Pierre-Marie Pédrot
2020-09-28Remove the ocamlformat git hook.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 09:29:47 +0000