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
*
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Pierre-Marie Pédrot
2018-07-03
|
\
*
\
Merge PR #7942: Extend readme with 'beginners guide'
Théo Zimmermann
2018-07-03
|
\
\
*
\
\
Merge PR #7974: Fix default.nix following a package renaming.
Vincent Laporte
2018-07-03
|
\
\
\
*
\
\
\
Merge PR #7977: allow `make check` to succeed when -prefix is given to ./conf...
Emilio Jesus Gallego Arias
2018-07-03
|
\
\
\
\
*
\
\
\
\
Merge PR #7703: Add an option to force parameters to be uniform
Matthieu Sozeau
2018-07-02
|
\
\
\
\
\
|
|
|
|
|
*
Add Equations overlay
Matthieu Sozeau
2018-07-02
*
|
|
|
|
|
Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions
Théo Zimmermann
2018-07-02
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7965: doc: Fix typesetting in Gallina extensions
Théo Zimmermann
2018-07-02
|
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
Clean up documentation around beginner's guide.
Siddharth Bhat
2018-07-02
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
[envars] honor env variable COQLIB
Enrico Tassi
2018-07-02
|
|
|
|
|
|
*
hints: add Hint Variables/Constants Opaque/Transparent commands
Matthieu Sozeau
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
|
\
\
\
\
\
\
|
|
|
|
|
|
*
Adding back ocp-index to default.nix.
Théo Zimmermann
2018-07-02
|
|
|
|
|
|
*
Fix default.nix following a package renaming.
Théo Zimmermann
2018-07-02
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Document option Uniform Inductive Parameters
Jasper Hugunin
2018-07-01
|
|
|
|
|
*
Add test for Uniform Inductive Parameters
Jasper Hugunin
2018-07-01
|
|
|
|
|
*
Add flag Uniform Inductive Parameters
Jasper Hugunin
2018-07-01
|
|
|
|
|
*
Implement uniform parameters in ComInductive
Jasper Hugunin
2018-07-01
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
[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
|
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
doc: typesetting and hyperlinks in Syntax Extensions
Lysxia
2018-06-30
*
|
|
|
|
|
|
|
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
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
doc: Fix typesetting in Gallina extensions
Lysxia
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
[next]
Pierre-Marie Pédrot
Théo Zimmermann
Vincent Laporte
Emilio Jesus Gallego Arias
Matthieu Sozeau
Siddharth Bhat
Enrico Tassi
Matthieu Sozeau
Jasper Hugunin
Lysxia
Hugo Herbelin
Maxime Dénès