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-25
Merge PR #9249: Fixing printing bug due to using equality wrongly checking ha...
Emilio Jesus Gallego Arias
2018-12-25
[ci] [appveyor] Pass -j2 to Appveyor's build.
Emilio Jesus Gallego Arias
2018-12-25
Merge PR #9278: [ci] Annotate plugins and libraries.
Emilio Jesus Gallego Arias
2018-12-25
Fixing printing bug due to using equality ill-checking hash key of kernel name.
Hugo Herbelin
2018-12-25
Adding a comparison combinator for pairs.
Hugo Herbelin
2018-12-25
[ssrmatching] update license banner (fix #9281)
Enrico Tassi
2018-12-23
[ci] Annotate plugins and libraries.
Théo Zimmermann
2018-12-23
Remove dead code from CClosure.
Pierre-Marie Pédrot
2018-12-23
Merge PR #9243: Fix line ending issues (azure related)
Michael Soegtrop
2018-12-22
Merge PR #9248: Fix #7904: update proofview env after ltac constr:()
Pierre-Marie Pédrot
2018-12-21
Merge PR #9247: Fix typo in gallina specification language doc
Théo Zimmermann
2018-12-21
Merge PR #9266: Make @SkySkimmer an owner of test-suite/report.sh
Théo Zimmermann
2018-12-21
Move lint job to gitlab
Gaëtan Gilbert
2018-12-21
Fix #9240: Register for IDProp causes anomaly when non constant
Gaëtan Gilbert
2018-12-21
Merge PR #9265: Do not exclude "opened" bugs from report
Gaëtan Gilbert
2018-12-21
Merge PR #9183: List members of the code of conduct enforcement team.
Matthieu Sozeau
2018-12-21
Make @SkySkimmer an owner of test-suite/report.sh
Maxime Dénès
2018-12-21
Do not exclude "opened" bugs from report
Maxime Dénès
2018-12-21
Fix shallow flag in vernac state
Maxime Dénès
2018-12-21
Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.
Maxime Dénès
2018-12-20
Make diffs work for more input strings
Jim Fehrle
2018-12-20
Relicense to Unlicense
Gaëtan Gilbert
2018-12-20
Merge PR #8488: Warning when using automatic template polymorphism
Pierre-Marie Pédrot
2018-12-20
Fix line ending issues
Gaëtan Gilbert
2018-12-20
Merge PR #9200: [ssr] make `>` stand alone
Maxime Dénès
2018-12-19
Fix #7904: update proofview env after ltac constr:()
Gaëtan Gilbert
2018-12-19
Add CHANGES for auto-template warning.
Gaëtan Gilbert
2018-12-19
Put #[universes(template)] in outputs tests
Gaëtan Gilbert
2018-12-19
Put #[universes(template)] on all auto template spots in stdlib
Gaëtan Gilbert
2018-12-19
warn when using auto template, funind never uses template poly
Gaëtan Gilbert
2018-12-19
Merge PR #9139: [engine] Allow debug printers to access the environment.
Pierre-Marie Pédrot
2018-12-19
Merge PR #9159: Make ugraph implementation abstract wrt universe specifics
Pierre-Marie Pédrot
2018-12-19
Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names in...
Pierre-Marie Pédrot
2018-12-19
Merge PR #9237: Add Map.find_opt
Pierre-Marie Pédrot
2018-12-19
[doc] typo
Enrico Tassi
2018-12-19
coqchk: fix check for kelim with functors
Gaëtan Gilbert
2018-12-19
Fix typo in gallina specification language doc
yudetamago
2018-12-19
Merge PR #9081: [dune] A new Makefile.dune target for each package (coq, coqi...
Théo Zimmermann
2018-12-19
[dune] Add targets for Coq individual packages.
Emilio Jesus Gallego Arias
2018-12-18
Merge PR #9223: Fix universe restriction in delayed mode.
Pierre-Marie Pédrot
2018-12-18
[ssr] make > a stand alone intro pattern
Enrico Tassi
2018-12-18
Merge PR #6705: [ssr] extended intro patterns
Cyril Cohen
2018-12-18
Fixes #9229 (Infix not robust wrt choice of variable names).
Hugo Herbelin
2018-12-18
[ssr] new test by Arthur Charguéraud
Enrico Tassi
2018-12-18
[ssr] extended intro patterns: + > [^] /ltac:
Enrico Tassi
2018-12-18
[arguments] cleanup
Enrico Tassi
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
Add comment to acyclicgraph API
Gaëtan Gilbert
2018-12-18
Merge PR #9160: Avoid user-given names in automatic introduction of binders
Pierre-Marie Pédrot
[prev]
[next]