aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
An identifier starting with _ deactivates the warning. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: Matafou Ack-by: ejgallego
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: Blaisorblade Ack-by: herbelin
2020-10-02More details in the documentation of native arraysVincent Semeria
Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Add persistent data structure Update doc/sphinx/language/core/primitive.rst Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-02Merge PR #13054: {new,setoid_}ring -> ringcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-app[bot]
Reviewed-by: ejgallego
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
Reviewed-by: SkySkimmer
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
Reviewed-by: ppedrot
2020-09-30Merge PR #13032: More precise information when unification fails because of ↵Pierre-Marie Pédrot
incompatible candidates Reviewed-by: ppedrot
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
It was not documented, not properly tested and thus likely buggy. Judging from the code alone I spotted already one potential bug. Further more it was prominently making use of the infamous "arbitrary term as hint" feature. Since the only user in our CI seems to be a math-classes file that introduced the feature under a claim of "cleanup", I believe we can safely remove it without anyone noticing.
2020-09-30interp_context_evars: removed unused [shift] argumentGaëtan Gilbert
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
Fix #13109
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
Reviewed-by: jfehrle
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
A commit at 2003-03-13 changed the lemma name. https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
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]
Reviewed-by: gares
2020-09-29Merge PR #13039: Lint stdlib with -mangle-names #3coqbot-app[bot]
Reviewed-by: anton-trunov
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a ↵coqbot-app[bot]
lonely notation at printing time. Reviewed-by: ejgallego Ack-by: maximedenes
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]
Reviewed-by: vbgl
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-28More precise information when unification fails because of incompatible ↵Hugo Herbelin
candidates. We also show the incompatible contender. Ideally, we should also remember the source of the other contender.
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
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
This would cause issues in noninteractive mode. For example, when using Drop, the first character of the OCaml code would be read by Coq's REPL instead of OCaml's REPL. The peek_string function is quite inefficient, since the Stream module does not provide any good function to lookup arbitrary characters (or to push back characters).
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
This commit also prevents quotations using "(" and "[" from gobbling sentences. As a consequence, dynamically-registered quotations can no longer modify where Coq sentences stop.
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ↵coqbot-app[bot]
GC (fix #12636). Reviewed-by: maximedenes Ack-by: bgregoir Ack-by: proux01
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
Reviewed-by: Zimmi48
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]
a context. Reviewed-by: mattam82
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
Reviewed-by: ejgallego
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of ↵Pierre-Marie Pédrot
quotations at printing time Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:54:18 +0000