index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-02-17
Merge PR #9506: Remove some non tailrec List.map from CList implementations
Pierre-Marie Pédrot
2019-02-16
Deprecated duplicated explicitation_eq
Jasper Hugunin
2019-02-14
Merge PR #9571: Document the now_show tactic.
Clément Pit-Claudel
2019-02-14
[coqlib] Remove `-boot` option for setting the coqlib
Emilio Jesus Gallego Arias
2019-02-14
Document the now_show tactic.
Théo Zimmermann
2019-02-14
Merge PR #9502: Remove nondeterministic tests
Théo Zimmermann
2019-02-14
Merge PR #9542: [Manual] Don’t use `Undo`; and other cleaning
Théo Zimmermann
2019-02-14
[Manual] Fix a reference
Vincent Laporte
2019-02-14
[Manual] Clean examples for `apply`
Vincent Laporte
2019-02-14
[Manual] Don’t use `Undo` in ssreflect examples
Vincent Laporte
2019-02-14
[Manual] Clean examples about `inversion` tactic
Vincent Laporte
2019-02-13
Merge PR #9554: Don't save expected failure logs from opened/ bugs.
Maxime Dénès
2019-02-13
Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...
Maxime Dénès
2019-02-13
[ssr] move shorter Canonical to Coq proper
Enrico Tassi
2019-02-13
more tests
Enrico Tassi
2019-02-13
refactor grammar
Enrico Tassi
2019-02-13
Fix #9432: canonical structure and coercion accept universe binders.
Gaëtan Gilbert
2019-02-13
Merge PR #9564: Fix small errors in cic.rst (3rd)
Théo Zimmermann
2019-02-13
Merge PR #9553: Sphinx various fixing of failing commands
Théo Zimmermann
2019-02-13
Merge PR #9557: [ssreflect] Export more parsing witnesses.
Enrico Tassi
2019-02-13
Merge PR #9173: [tactics] Remove dependency of abstract on global proof state.
Maxime Dénès
2019-02-12
Merge PR #9548: Almost fully type-safe gramlib implementation
Emilio Jesus Gallego Arias
2019-02-12
Merge PR #9563: Improve the documentation of auto.
Clément Pit-Claudel
2019-02-12
Fix failing coqtops in syntax-extensions.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in tactics.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in ssreflect-proof-language.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in ltac.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in coqide.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in gallina-specification-language.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in gallina-extensions.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in coq-library.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in cic.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops universe-polymorphism.rst
Gaëtan Gilbert
2019-02-12
Improve the documentation of auto.
Théo Zimmermann
2019-02-12
[tactics] Remove dependency of abstract on global proof state.
Emilio Jesus Gallego Arias
2019-02-12
Fix failing coqtops in ring.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in micromega.rst (the main one requires csdp)
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in generalized-rewriting.rst
Gaëtan Gilbert
2019-02-12
Fix failing coqtops in extended-pattern-matching.rst
Gaëtan Gilbert
2019-02-12
Fix undefined SPHINX_DEPS when QUICK
Gaëtan Gilbert
2019-02-12
Fix doc for coqtop:: undo
Gaëtan Gilbert
2019-02-12
Increase sphinx recursion limit
Gaëtan Gilbert
2019-02-11
Merge PR #9551: Small typos in the documentation.
Théo Zimmermann
2019-02-11
Merge PR #9540: [ssr] keep user annotation on views (fix #9538)
Cyril Cohen
2019-02-11
[ssreflect] Export more parsing witnesses.
Emilio Jesus Gallego Arias
2019-02-11
Merge PR #9544: [coqargs] Minor refactoring of error functions.
Enrico Tassi
2019-02-11
Don't save expected failure logs from opened/ bugs.
Gaëtan Gilbert
2019-02-11
Merge PR #9531: [test-suite] Improve test for async workers.
Enrico Tassi
2019-02-11
Small typos in the documentation.
Martin Bodin
2019-02-11
[ide] fix unconditional goto-point on editing an error (fix #9488)
Enrico Tassi
[prev]
[next]