index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-12-18
Fixes #9229 (Infix not robust wrt choice of variable names).
Hugo Herbelin
2018-12-18
Merge PR #9218: [STM] Better protection for cur_id
Enrico Tassi
2018-12-18
Merge PR #9222: Fix classification of Set Default Proof Mode.
Enrico Tassi
2018-12-18
Merge PR #9160: Avoid user-given names in automatic introduction of binders
Pierre-Marie Pédrot
2018-12-18
Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ma...
Pierre-Marie Pédrot
2018-12-18
Merge PR #9215: Set up CI with Azure Pipelines
Emilio Jesus Gallego Arias
2018-12-17
Merge PR #9153: [api] Move reduction modules to `tactics`
Pierre-Marie Pédrot
2018-12-17
[STM] Better protection for cur_id
Maxime Dénès
2018-12-17
Merge PR #9238: CI: simple-io now depends on ext-lib
Emilio Jesus Gallego Arias
2018-12-17
Set up CI with Azure Pipelines
Gaëtan Gilbert
2018-12-17
simple-io now depends on ext-lib
Gaëtan Gilbert
2018-12-17
Merge PR #8856: [gitlab] Test Ocaml trunk.
Gaëtan Gilbert
2018-12-17
Fix git line ending conversion in windows
Gaëtan Gilbert
2018-12-17
Fix classification of Set Default Proof Mode.
Gaëtan Gilbert
2018-12-17
Merge PR #9206: [stm] join the tip of the document even when fixing a proof (...
Emilio Jesus Gallego Arias
2018-12-17
Merge PR #9219: [STM] Fix logic of debug DAG printer
Enrico Tassi
2018-12-17
Merge PR #9220: Move shallow state logic to the function preparing state for ...
Enrico Tassi
2018-12-17
CoqIDE: Restoring configuration of default width/height of main window.
Hugo Herbelin
2018-12-16
Merge PR #9172: [proof] Rework proof interface.
Pierre-Marie Pédrot
2018-12-15
Avoid explicit names in binders for automatic intros
Jasper Hugunin
2018-12-14
Merge PR #9073: [sphinx] No more undocumented objects.
Clément Pit-Claudel
2018-12-14
[dune] [gitlab] Test OCaml trunk.
Emilio Jesus Gallego Arias
2018-12-14
Merge PR #9147: [dune] [doc] Support for building the reference manual with D...
Théo Zimmermann
2018-12-14
[proof] Rework proof interface.
Emilio Jesus Gallego Arias
2018-12-14
Update pinned nixpkgs to use Dune 1.6.
Théo Zimmermann
2018-12-14
Turn warning on for undocumented objects. Closes #7602.
Théo Zimmermann
2018-12-14
Fix the SSReflect chapter regarding objects without bodies.
Théo Zimmermann
2018-12-14
Do not raise object without body warning for prodn objects.
Théo Zimmermann
2018-12-13
Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost o...
Gaëtan Gilbert
2018-12-13
Merge PR #9194: Fixing uses of sed in #8985 which do not work on MacOS X
Matthieu Sozeau
2018-12-13
Fixing uses of sed which do not work on MacOS X.
Hugo Herbelin
2018-12-13
Merge PR #9117: Accept argument names for extra arguments with "extra scopes"
Matthieu Sozeau
2018-12-13
Add overlay
Maxime Dénès
2018-12-13
Merge PR #9210: Fix issue #9176 : Windows: change cygwin repo
Théo Zimmermann
2018-12-13
Merge PR #9211: Fixing incorrect mention of coercions as being part of the in...
Théo Zimmermann
2018-12-13
[dune] [doc] Support for building the reference manual with Dune.
Emilio Jesus Gallego Arias
2018-12-13
Merge PR #9032: checker: check inductive types by roundtrip through the kernel.
Pierre-Marie Pédrot
2018-12-13
Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as patter...
Pierre-Marie Pédrot
2018-12-13
Merge PR #9169: [rtauto] [auto] Use new proof engine.
Pierre-Marie Pédrot
2018-12-13
Merge PR #9217: [ci] [appveyor] Temporally disable test suite on Appveyor.
Gaëtan Gilbert
2018-12-13
[test] for join when error resiliency on and async-proofs off
Enrico Tassi
2018-12-13
[stm] join: check no error states are part of the document
Enrico Tassi
2018-12-13
Merge PR #9196: Document the deprecation of hint declaration withou database ...
Maxime Dénès
2018-12-13
[test] for #9204
Enrico Tassi
2018-12-13
[stm] join the tip of the document even when fixing a proof (fix #9204)
Enrico Tassi
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-12-13
[STM] Fix logic of debug DAG printer
Maxime Dénès
2018-12-13
Merge PR #8096: Higher-level libobject API for objects with fixed scopes
Enrico Tassi
2018-12-13
[ci] [appveyor] Temporally disable test suite on Appveyor.
Emilio Jesus Gallego Arias
2018-12-12
Merge PR #9101: Fix 8922 again
Hugo Herbelin
[next]