index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-10-26
Merge PR #13137: [ltac] Avoid magic numbers
coqbot-app[bot]
2020-10-25
Merge PR #12936: Convert misc chapters to prodn, update syntax
coqbot-app[bot]
2020-10-24
Convert misc chapters to prodn
Jim Fehrle
2020-10-24
Merge PR #13263: Correct doc using :>>
coqbot-app[bot]
2020-10-23
Correct doc using :>>
Gaëtan Gilbert
2020-10-23
Merge PR #13261: Fix overlay merge command
coqbot-app[bot]
2020-10-23
[declare] Remove recursive declaration from non-recursive functions
Emilio Jesus Gallego Arias
2020-10-23
Fix overlay merge command
Gaëtan Gilbert
2020-10-23
Force-delete pr branches.
Théo Zimmermann
2020-10-23
Merge PR #13177: Automatically merge overlays with most recent upstream version
coqbot-app[bot]
2020-10-22
Make no match/multiple match for tacn/cmd an error
Jim Fehrle
2020-10-22
Merge PR #11924: Add style for smallcaps.
coqbot-app[bot]
2020-10-22
Remove test-suite/bugs/opened/bug_3395.v: not a bug
Gaëtan Gilbert
2020-10-22
Fix printing of wit_constr and some ssr problems with printing empty lists
Lasse Blaauwbroek
2020-10-22
Make sure that setoid_rewrite passes state to subgoals
Lasse Blaauwbroek
2020-10-22
Micro-optimization in Control.check_for_interrupt.
Pierre-Marie Pédrot
2020-10-22
Merge PR #13243: Fix bench variables
Pierre-Marie Pédrot
2020-10-22
Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env.
Vincent Laporte
2020-10-22
[default.nix] Propagate OCaml and findlib to user env.
Théo Zimmermann
2020-10-22
Merge PR #13130: setoid_rewrite: record generated name when rewriting under l...
Pierre-Marie Pédrot
2020-10-22
Fix bench variables
Gaëtan Gilbert
2020-10-22
Merge PR #13198: [coqinit] Respect order of ML includes
coqbot-app[bot]
2020-10-21
[coqinit] Cosmetics on long list append.
Emilio Jesus Gallego Arias
2020-10-21
[coqinit] Respect order of ML includes
Emilio Jesus Gallego Arias
2020-10-21
Merge PR #13222: Bench: move variables to the script
Pierre-Marie Pédrot
2020-10-21
Add overlays.
Pierre-Marie Pédrot
2020-10-21
Add missing deprecations in Projection API.
Pierre-Marie Pédrot
2020-10-21
Document the signatures of quotient names in the API.
Pierre-Marie Pédrot
2020-10-21
Introduce the missing dual name quotient modules in Environ.
Pierre-Marie Pédrot
2020-10-21
Code factorization in Names.
Pierre-Marie Pédrot
2020-10-21
Similar introduction of a Construct module in the Names API.
Pierre-Marie Pédrot
2020-10-21
Introduce an Ind module in the Names API.
Pierre-Marie Pédrot
2020-10-21
Rename the GlobRef comparison modules following the standard pattern.
Pierre-Marie Pédrot
2020-10-21
Same little game with Projection.
Pierre-Marie Pédrot
2020-10-21
Deprecate the non-qualified equality functions on kerpairs.
Pierre-Marie Pédrot
2020-10-21
Introduce a dummy name quotient API.
Pierre-Marie Pédrot
2020-10-21
Merge PR #13118: [type classes] Simplify cl_context
Pierre-Marie Pédrot
2020-10-21
Merge PR #13201: Report a useful error for dependent destruction
Pierre-Marie Pédrot
2020-10-21
Merge PR #12955: Reroot primitive arrays on access
coqbot-app[bot]
2020-10-20
Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loop
coqbot-app[bot]
2020-10-20
Merge PR #12648: [zify] support for int63
coqbot-app[bot]
2020-10-20
Merge PR #13180: Respect Print Universes when printing primitive arrays
coqbot-app[bot]
2020-10-20
Add some missing smallcaps.
Théo Zimmermann
2020-10-20
[zify] Use flag for Z.to_euclidean_division_equations.
Frédéric Besson
2020-10-20
[zify] Add support for Int63.int
Frédéric Besson
2020-10-19
Better message and avoid an infinite SPLICE loop
Jim Fehrle
2020-10-19
Bench: move variables to the script
Gaëtan Gilbert
2020-10-19
Restore the List.Smart.map original implementation.
Pierre-Marie Pédrot
2020-10-19
Add style for smallcaps.
Théo Zimmermann
2020-10-19
Merge PR #13208: Support "Solve Obligations of <ident>"
coqbot-app[bot]
[prev]
[next]