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-09-23
Merge PR #12977: Statically ensure that only polymophic hint terms come with ...
coqbot-app[bot]
2020-09-23
Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)
coqbot-app[bot]
2020-09-23
Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotatio...
Pierre-Marie Pédrot
2020-09-23
Merge PR #12847: Tactics inversion and replace work with eq in type
Pierre-Marie Pédrot
2020-09-22
Merge PR #13061: fix build:quick and build:base+async artifacts
coqbot-app[bot]
2020-09-22
Merge PR #13067: Setting default value for Display Parentheses off in CoqIDE
coqbot-app[bot]
2020-09-22
Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...
coqbot-app[bot]
2020-09-22
Adding change log for #12794 and #13067.
Hugo Herbelin
2020-09-22
Setting default value for Display Parentheses off in CoqIDE.
Hugo Herbelin
2020-09-22
Add overlay for Equations.
Hugo Herbelin
2020-09-22
Adding change log for #13028.
Hugo Herbelin
2020-09-22
Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.
Hugo Herbelin
2020-09-22
Merge PR #13046: Small optimization of acyclic graph merge operation
coqbot-app[bot]
2020-09-22
Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling git...
coqbot-app[bot]
2020-09-22
Merge PR #13049: [configure] Fix version checks for lablgtk and zarith
coqbot-app[bot]
2020-09-22
Merge PR #13063: Make print-pretty-timed robust against non-output-sync logs
coqbot-app[bot]
2020-09-21
Merge PR #13057: Adding debugging printers for Intmap
coqbot-app[bot]
2020-09-21
Make print-pretty-timed robust against non-output-sync logs
Jason Gross
2020-09-21
Bump nixpkgs to get zarith 1.10.
Théo Zimmermann
2020-09-21
Merge PR #12723: dune: pass -bin-annot to configure
coqbot-app[bot]
2020-09-21
fix build:quick and build:base+async artifacts
Gaëtan Gilbert
2020-09-19
Merge PR #13052: Clean up Dnet implementation
Hugo Herbelin
2020-09-18
Merge PR #13055: Fix Removed in Sphinx 4 deprecations.
coqbot-app[bot]
2020-09-18
Merge PR #12963: Formally deprecate the double induction tactic.
Hugo Herbelin
2020-09-18
Adding debugging printers for Intmap.
Hugo Herbelin
2020-09-18
Merge PR #13051: Improve `simple apply` example
coqbot-app[bot]
2020-09-18
Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOM
coqbot-app[bot]
2020-09-18
Fix Removed in Sphinx 4 deprecations.
Théo Zimmermann
2020-09-18
Make `simple apply in ...` point to `simple apply`
Maxime Dénès
2020-09-18
[ci] [dmesg] save as artifact
Enrico Tassi
2020-09-18
Improve `simple apply` example
Maxime Dénès
2020-09-18
Merge PR #12610: [leminv] [declare] Use higher-level Declare API.
Pierre-Marie Pédrot
2020-09-18
Remove unused API from Dn.
Pierre-Marie Pédrot
2020-09-18
Clean up a bit the implemenation of dnets.
Pierre-Marie Pédrot
2020-09-18
Remove dead code in dnets.
Pierre-Marie Pédrot
2020-09-18
Merge PR #13027: [vernac] Don't allow attributes on print / check
coqbot-app[bot]
2020-09-17
[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow.
Théo Zimmermann
2020-09-17
Merge PR #13007: [build] Don't link `num` anymore in Coq
coqbot-app[bot]
2020-09-17
[configure] Fix version checks for lablgtk and zarith
Emilio Jesus Gallego Arias
2020-09-17
Be more efficient when generating the merge of ltle maps in AcyclicGraph.
Pierre-Marie Pédrot
2020-09-17
Do not allocate intermediate sets in universe refreshing.
Pierre-Marie Pédrot
2020-09-17
[leminv] Use higher-level Declare API.
Emilio Jesus Gallego Arias
2020-09-17
[leminv] Remove unused catch.
Emilio Jesus Gallego Arias
2020-09-17
[install] Rewording of primitive floats.
Emilio Jesus Gallego Arias
2020-09-17
[build] Don't link `num` anymore in Coq
Emilio Jesus Gallego Arias
2020-09-17
Merge PR #13024: [CI] Always upload artifacts
coqbot-app[bot]
2020-09-17
[ci] call dmesg after quick/async jobs to detect OOM
Enrico Tassi
2020-09-17
Formally deprecate the double induction tactic.
Pierre-Marie Pédrot
2020-09-16
Merge PR #13008: Use fresher names in eqschemes
Hugo Herbelin
2020-09-16
Merge PR #13015: Propagate zarith dependency.
Vincent Laporte
[next]