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-04-29
correct script name create_overlays.sh
Olivier Laurent
2020-04-29
Merge the call to tclEFFECTS into find_scheme.
Pierre-Marie Pédrot
2020-04-29
Remove dead user-facing code in scheme generation.
Pierre-Marie Pédrot
2020-04-29
CI: ext-lib is at coq-community now
Antonio Nikishaev
2020-04-28
Merge PR #12193: Close files in fetch_delayed
Emilio Jesus Gallego Arias
2020-04-28
[doc] [sphinx] Be silent when running latexmk
Emilio Jesus Gallego Arias
2020-04-28
[doc] [sphinx] Run in silent mode by default
Emilio Jesus Gallego Arias
2020-04-28
Merge PR #12183: Suggestion of improvement for the Allow SProp error message.
Gaëtan Gilbert
2020-04-28
Merge PR #12164: Stop relying on side-effects for recursive scheme declaration
Emilio Jesus Gallego Arias
2020-04-28
Add comment about decide equality dependence computation.
Pierre-Marie Pédrot
2020-04-28
Return an option in lookup_scheme.
Pierre-Marie Pédrot
2020-04-28
Stop relying on side-effects for recursive scheme declaration.
Pierre-Marie Pédrot
2020-04-28
Merge PR #12003: Improve error messages for Set and Unset commands.
Emilio Jesus Gallego Arias
2020-04-28
Merge PR #12188: Do not delay the loading of the library_disk field when requ...
Emilio Jesus Gallego Arias
2020-04-28
Merge PR #12189: Fix an ordering bug in the CODEOWNERS file following #11529.
Emilio Jesus Gallego Arias
2020-04-28
Close files in fetch_delayed
Gaëtan Gilbert
2020-04-28
Merge PR #11718: Convert syntax extensions chapter to prodn
Théo Zimmermann
2020-04-27
[ci] Add coq-tools to the CI
Jason Gross
2020-04-27
Merge PR #12073: Split off Nsatz tactic part into Nsatz_tactic
Pierre-Marie Pédrot
2020-04-27
Merge PR #12175: Calculation speed of Cauchy reals
Michael Soegtrop
2020-04-27
Merge PR #12160: CoqIDE: Avoid invalidation of an iterator in insert callback
Pierre-Marie Pédrot
2020-04-27
Merge PR #12168: [dune] Fix dependencies of refman.
Emilio Jesus Gallego Arias
2020-04-27
Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in...
Clément Pit-Claudel
2020-04-27
Merge PR #12132: [refman] Remove references to omega from Tactics chapter.
Vincent Laporte
2020-04-27
Fix an ordering bug in the CODEOWNERS file following #11529.
Théo Zimmermann
2020-04-27
Do not delay the loading of the library_disk field when requiring libraries.
Pierre-Marie Pédrot
2020-04-27
Merge PR #12181: Add sphinx-clean option to force full sphinx rebuild
Théo Zimmermann
2020-04-27
Further documentation improvements.
Théo Zimmermann
2020-04-27
Improve the Allow SProp error message.
Théo Zimmermann
2020-04-26
Convert syntax extensions chapter to prodn
Jim Fehrle
2020-04-26
Add sphinx_clean option to force full sphinx rebuild
Jim Fehrle
2020-04-26
Merge PR #12092: Implement a name-based representation for vo files.
Enrico Tassi
2020-04-26
Merge PR #12176: Doc: extend example for induction a bit
Théo Zimmermann
2020-04-26
Document the signing procedure of released binary packages.
Pierre-Marie Pédrot
2020-04-26
constructive square root
Vincent Semeria
2020-04-26
Open object files in binary mode.
Pierre-Marie Pédrot
2020-04-26
Tweak a comment on the low-level objfile API.
Pierre-Marie Pédrot
2020-04-26
Move the ObjFile module to its own file.
Pierre-Marie Pédrot
2020-04-26
Implement a name-based representation for vo files.
Pierre-Marie Pédrot
2020-04-26
Merge PR #12178: Fix recursively vs corecursively defined message
Pierre-Marie Pédrot
2020-04-25
Fix recursively vs corecursively defined message
Tej Chajed
2020-04-25
Doc: extend example for induction a bit
Gaëtan Gilbert
2020-04-25
Merge PR #12173: CoqIDE: Revert overzealous application of language-based hig...
Pierre-Marie Pédrot
2020-04-24
Make the nsatz test-suite pass
Jason Gross
2020-04-24
[nsatz] Use Export rather than Include
Jason Gross
2020-04-24
Add memory stats to tables by default
Jason Gross
2020-04-24
Split off Nsatz tactic part into NsatzTactic
Jason Gross
2020-04-24
CoqIDE: Revert overzealous application of language-based highlighting in #12169.
Hugo Herbelin
2020-04-24
[dune] Fix dependencies of refman.
Théo Zimmermann
2020-04-24
Merge PR #12156: Document `+` in polymorphic universe levels
Théo Zimmermann
[prev]
[next]