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-11-15
Merge PR #13356: Make the universe of primitive arrays irrelevant
Pierre-Marie Pédrot
2020-11-14
Merge PR #13369: Move destructuring let syntax closer to its documentation.
coqbot-app[bot]
2020-11-14
Move destructuring let syntax closer to its documentation.
Théo Zimmermann
2020-11-13
Merge PR #13358: Merge the Linked / LinkedInteractive native link information...
coqbot-app[bot]
2020-11-13
Make the universe of primitive arrays irrelevant
Gaëtan Gilbert
2020-11-13
Remove unused CClosure.FNativeEntries.farray
Gaëtan Gilbert
2020-11-13
Merge PR #12420: [stdlib] Decidable instance for negation
coqbot-app[bot]
2020-11-12
Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop
coqbot-app[bot]
2020-11-12
Change Dumpglob.pause and Dumpglob.continue into push and pop
Lasse Blaauwbroek
2020-11-12
Merge PR #13318: Turn ssr proxy notation for supporting second-order/contextu...
coqbot-app[bot]
2020-11-12
Merge PR #13361: Move last changelog entry for 8.12.1.
coqbot-app[bot]
2020-11-12
Move last changelog entry for 8.12.1.
Théo Zimmermann
2020-11-12
Merge PR #13359: Print failed test suite logs in CI
coqbot-app[bot]
2020-11-12
Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...
coqbot-app[bot]
2020-11-12
Merge PR #13355: Fix Iris CI script
coqbot-app[bot]
2020-11-12
Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.
coqbot-app[bot]
2020-11-12
Print failed test suite logs in CI
Gaëtan Gilbert
2020-11-12
Merge the Linked and LinkedInteractive constructors.
Pierre-Marie Pédrot
2020-11-12
Statically ensure that the native interactive flag is always set to true.
Pierre-Marie Pédrot
2020-11-12
Statically ensure that native update locations are of form Linked*.
Pierre-Marie Pédrot
2020-11-12
Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...
Pierre-Marie Pédrot
2020-11-12
Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I
coqbot-app[bot]
2020-11-12
Add the test as a misc script.
Pierre-Marie Pédrot
2020-11-12
Add documentation about the soundness bug.
Pierre-Marie Pédrot
2020-11-12
Fix #13330: Kernel messes with polymorphic side-effects.
Pierre-Marie Pédrot
2020-11-12
Fix Iris CI script
Gaëtan Gilbert
2020-11-12
Add changelog for #13345.
Hugo Herbelin
2020-11-12
Clarifying the role of Add ML Path vs -I (see #13344).
Hugo Herbelin
2020-11-12
Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply
coqbot-app[bot]
2020-11-11
Add changelog for #13351.
Hugo Herbelin
2020-11-11
Addressing #13349: accept Search on subparts of ident, not only on subidents.
Hugo Herbelin
2020-11-10
Merge PR #13335: Fix running unit tests with dune compiled coq
coqbot-app[bot]
2020-11-10
Merge PR #13315: Convert logic chapter to prodn
coqbot-app[bot]
2020-11-10
Convert logic.rst to prodn
Jim Fehrle
2020-11-10
Fix running unit tests with dune compiled coq
Gaëtan Gilbert
2020-11-10
Merge PR #13325: [compat] remove 8.10
coqbot-app[bot]
2020-11-10
Merge PR #13322: [obligation] Properly handle no obligations on `Next Obligat...
coqbot-app[bot]
2020-11-10
Merge PR #13297: Remove the native symbol registering from the safe environment.
coqbot-app[bot]
2020-11-09
Add additional escape sequences for notations
Jim Fehrle
2020-11-09
Add global version of OPTINREF
Jim Fehrle
2020-11-09
Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...
coqbot-app[bot]
2020-11-09
Merge PR #13327: Fix documentation of Ltac ::=
coqbot-app[bot]
2020-11-09
[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.
Théo Zimmermann
2020-11-09
[obligation] Proper handle no obligations on `Next Obligation`
Emilio Jesus Gallego Arias
2020-11-09
Remove virtually unused replace rule.
Théo Zimmermann
2020-11-09
Fix #5226: Add index entry for ::=.
Théo Zimmermann
2020-11-09
Fix indentation of todo in Ltac chapter.
Théo Zimmermann
2020-11-09
Remove the native symbol registering from the safe environment.
Pierre-Marie Pédrot
2020-11-09
[compat] remove 8.10
Enrico Tassi
2020-11-09
Merge PR #13310: Fix macOS CI on Azure.
coqbot-app[bot]
[next]