index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
[ci] [docker] Make sure we don't install optional packages with apt.
Emilio Jesus Gallego Arias
2018-07-02
*
Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points...
Emilio Jesus Gallego Arias
2018-07-02
|
\
*
\
Merge PR #7961: [api] Fix wrong deprecation warning (#7915)
Enrico Tassi
2018-07-02
|
\
\
|
*
|
[api] Fix wrong deprecation warning (#7915)
Emilio Jesus Gallego Arias
2018-07-01
|
/
/
*
|
Merge PR #7964: Document that GITURL variables shouldn't have a trailing .git...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
*
\
\
Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, Z...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
\
*
\
\
\
Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
\
\
*
\
\
\
\
Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break...
Emilio Jesus Gallego Arias
2018-07-01
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7960: [build] Remove target binary before copy.
Enrico Tassi
2018-06-30
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7949: Split the Ssrmatching module between code and grammar rules.
Enrico Tassi
2018-06-30
|
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
Split the Ssrmatching module between code and grammar rules.
Pierre-Marie Pédrot
2018-06-30
|
/
/
/
/
/
/
/
|
|
|
|
|
|
*
Adding an overlay for the PR.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Documenting the transition strategy of GEXTEND.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_tactic to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_toplevel to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_vernac to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_proofs to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_constr to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Port g_prim to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
2018-06-29
|
|
|
|
|
|
*
Use a homebrew parser to replace the GEXTEND extension points of Camlp5.
Pierre-Marie Pédrot
2018-06-29
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Document that GITURL variables shouldn't have a trailing .git anymore.
Théo Zimmermann
2018-06-29
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7918: Mini-update of version history with recent changes.
Théo Zimmermann
2018-06-29
|
\
\
\
\
\
|
|
|
|
|
*
Splitting primitive numeral parser/printer for positive, N, Z into three files.
Hugo Herbelin
2018-06-29
|
|
|
*
|
|
Workaround to fix #7731 (printing not splitting line at break hint).
Hugo Herbelin
2018-06-29
|
|
|
|
|
/
|
|
|
|
/
|
|
|
|
|
*
Fixes #7712 (an anomaly in reporting bad recursive notation format).
Hugo Herbelin
2018-06-29
|
|
|
|
/
*
|
|
|
Merge PR #7080: Swapping Context and Constr and defining declarations on cons...
Maxime Dénès
2018-06-29
|
\
\
\
\
|
|
|
*
|
[build] Remove target binary before copy.
Emilio Jesus Gallego Arias
2018-06-29
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #7890: Inline a function from Quote used in setoid_ring.
Maxime Dénès
2018-06-29
|
\
\
\
\
*
\
\
\
\
Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retrokn...
Maxime Dénès
2018-06-29
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7950: Documentation for 8.8.1
Maxime Dénès
2018-06-29
|
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #7860: Fix #7704: Launching coqide through PATH fails.
Emilio Jesus Gallego Arias
2018-06-28
|
\
\
\
\
\
\
|
|
*
|
|
|
|
CHANGES for 8.8.1.
Théo Zimmermann
2018-06-28
|
|
*
|
|
|
|
Self-credit for the work done.
Théo Zimmermann
2018-06-28
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #7948: Syntax for naming an existential variable
Théo Zimmermann
2018-06-28
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.
Michael Soegtrop
2018-06-28
|
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
wrong sphinx syntax
Ambroise
2018-06-28
*
|
|
|
|
|
|
|
Merge PR #7946: Update maintainers for native/VM files in pretyping
Théo Zimmermann
2018-06-28
|
\
\
\
\
\
\
\
\
|
|
|
*
|
|
|
|
|
Update gallina-extensions.rst
Ambroise
2018-06-28
|
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Merge PR #7937: Mention Consortium in README
Théo Zimmermann
2018-06-28
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.
Théo Zimmermann
2018-06-28
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
Deprecate Environ.retroknowledge function in favor of the projection
Gaëtan Gilbert
2018-06-28
|
|
|
|
|
|
*
|
|
|
[env.env_rel_context.env_rel_ctx] -> [rel_context env]
Gaëtan Gilbert
2018-06-28
|
|
|
|
|
|
*
|
|
|
Make Environ.globals abstract.
Gaëtan Gilbert
2018-06-28
|
|
_
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.
Pierre-Marie Pédrot
2018-06-28
|
\
\
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
|
|
Update maintainers for native/VM files in pretyping
Maxime Dénès
2018-06-28
|
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #7866: Implementation of mutual records in the higher strata
Maxime Dénès
2018-06-28
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #7934: Add mit-plv/bedrock2-ci to CI
Emilio Jesus Gallego Arias
2018-06-28
|
\
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
Add mit-plv/bedrock2-ci to CI
Andres Erbsen
2018-06-27
|
/
/
/
/
/
/
/
/
/
/
*
|
|
|
|
|
|
|
|
|
Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)
Pierre-Marie Pédrot
2018-06-27
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #7939: Turn the CoqProject_file module into a pure ML file
Emilio Jesus Gallego Arias
2018-06-27
|
\
\
\
\
\
\
\
\
\
\
\
[next]
Emilio Jesus Gallego Arias
Enrico Tassi
Pierre-Marie Pédrot
Théo Zimmermann
Hugo Herbelin
Maxime Dénès
Michael Soegtrop
Ambroise
Gaëtan Gilbert
Andres Erbsen