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-04-29
Merge PR #10018: Document unshelve (#3225)
Théo Zimmermann
2019-04-29
Merge PR #10021: More robust timing test.
Enrico Tassi
2019-04-29
Test-suite: add a case for issue #9180
Vincent Laporte
2019-04-29
Revert #8187
Vincent Laporte
2019-04-29
Revert #9249
Vincent Laporte
2019-04-29
More robust timing test.
Jason Gross
2019-04-29
Merge PR #9997: CoqIDE: fix open-file dialog and icons on macOS
Enrico Tassi
2019-04-29
[meta] [dune] Fix discrepancies in plugin names
Emilio Jesus Gallego Arias
2019-04-28
Update behavior of -emacs to support showing diffs in ProofGeneral (master br...
Jim Fehrle
2019-04-29
Document unshelve (#3225)
Paolo G. Giarrusso
2019-04-28
Merge PR #10010: [ci/gitlab] Remove after_switch message (not useful anymore).
Emilio Jesus Gallego Arias
2019-04-28
Merge PR #9605: [coq_makefile] Enforce warn_error for plugins.
Gaëtan Gilbert
2019-04-28
[test-suite] Remove a test with a Timeout that fails frequently on CI.
Théo Zimmermann
2019-04-27
Updating CHANGES.
Hugo Herbelin
2019-04-27
CoqIDE, cosmetic: removing obsolete comments.
Hugo Herbelin
2019-04-27
CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899).
Hugo Herbelin
2019-04-27
Minor doc improvement.
Théo Zimmermann
2019-04-27
[refman] Fix typo.
Théo Zimmermann
2019-04-27
[ci/gitlab] Remove after_switch message (not useful anymore).
Théo Zimmermann
2019-04-27
Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.
Hugo Herbelin
2019-04-26
Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Emilio Jesus Gallego Arias
2019-04-26
Merge PR #9981: [dune] Build coqc.byte executable.
Théo Zimmermann
2019-04-26
Merge PR #9990: [opam] Use version to provide better package bounds.
Théo Zimmermann
2019-04-26
Merge PR #10001: Add a typing colon in the output of the Search ssreflect ver...
Enrico Tassi
2019-04-26
[opam] Use version to provide better package bounds.
Emilio Jesus Gallego Arias
2019-04-25
[vernac] [ast] Make location info an attribute of vernaculars.
Emilio Jesus Gallego Arias
2019-04-25
Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3
Emilio Jesus Gallego Arias
2019-04-25
CoqIDE: install icons on macOS
Vincent Laporte
2019-04-25
inferCumulativity: shortcut for all-Invariant inductives
Gaëtan Gilbert
2019-04-25
Add a typing colon in the output of the Search ssreflect vernacular
Erik Martin-Dorel
2019-04-25
Fix PKG in ide/.merlin.in for gtk3
Gaëtan Gilbert
2019-04-25
CoqIDE: fix open-file dialog on macOS
Vincent Laporte
2019-04-25
coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Enrico Tassi
2019-04-25
Merge Ltac2 plugin
Maxime Dénès
2019-04-25
Prepare merge into Coq
Maxime Dénès
2019-04-24
Merge PR #9988: [refman] Properly define token regexp.
Clément Pit-Claudel
2019-04-24
Merge PR #9989: [refman] Fix a quoting problem.
Clément Pit-Claudel
2019-04-24
[refman] Fix a quoting problem.
Théo Zimmermann
2019-04-24
[refman] Properly define token regexp.
Théo Zimmermann
2019-04-24
[coq_makefile] Enforce warn_error for plugins.
Emilio Jesus Gallego Arias
2019-04-24
Fix proof bullet error helper (nosuchgoal)
Gaëtan Gilbert
2019-04-24
[proof] Fix proof bullet error helper which was implemented as a hook
Emilio Jesus Gallego Arias
2019-04-24
Allocate only one evar when applying a group of conversion tactics.
Pierre-Marie Pédrot
2019-04-24
Code factorization in conversion tactics.
Pierre-Marie Pédrot
2019-04-24
[dune] Build coqc.byte executable.
Emilio Jesus Gallego Arias
2019-04-23
Deprecate the *_no_check variants of conversion tactics.
Pierre-Marie Pédrot
2019-04-23
Merge PR #9962: [native compiler] Encoding of constructors based on tags
Pierre-Marie Pédrot
2019-04-23
[ssr] set under's tactic argument at LEVEL 3
Erik Martin-Dorel
2019-04-23
[ssr] under: optimization of the tactic for (under eq_bigl => *)
Erik Martin-Dorel
2019-04-23
[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations
Erik Martin-Dorel
[prev]
[next]