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-10
For diffs, return exactly the characters that make up STRING and FIELD tokens
Jim Fehrle
2018-12-10
Fix #9091: don't show deleted compacted hypotheses twice in diff
Jim Fehrle
2018-12-10
Treat unmatched goals as new for diffs (highlighted)
Jim Fehrle
2018-12-10
[coq] Adapt to coq/coq#9172
Emilio Jesus Gallego Arias
2018-12-10
List members of the code of conduct enforcement team.
Théo Zimmermann
2018-12-10
[test-suite] Fail when the checker fails
Vincent Laporte
2018-12-10
[test-suite] Run `coqchk` on most test cases
Vincent Laporte
2018-12-10
[dune] Teach coq_dune about `.glob` and `.aux` files.
Emilio Jesus Gallego Arias
2018-12-10
Merge PR #9145: Do so that an error message follows the "Error:" header on th...
Emilio Jesus Gallego Arias
2018-12-10
Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.pack
Emilio Jesus Gallego Arias
2018-12-10
Merge PR #9177: add relation-algebra to CI test suite
Gaëtan Gilbert
2018-12-10
Merge PR #9106: [dune] Install coq libraries in `%{lib_root}/coq` instead of ...
Vincent Laporte
2018-12-10
Merge PR #7221: The usual order of strings.
Hugo Herbelin
2018-12-09
fix copy-paste error in CI_ARCHIVEURL
Christian Doczkal
2018-12-09
add relation-algebra to CI test suite
Christian Doczkal
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-12-08
[dune] Install coq libraries in `%{lib_root}/coq` instead of `lib`
Emilio Jesus Gallego Arias
2018-12-08
Do so that an error message follows the "Error:" header on the same line.
Hugo Herbelin
2018-12-07
Merge PR #8811: EConstr-aware functions to produce kernel entries
Pierre-Marie Pédrot
2018-12-06
Merge PR #9140: [ci] Add four color theorem proof to CI
Gaëtan Gilbert
2018-12-06
Revise API for global universes.
Gaëtan Gilbert
2018-12-06
High level functions to produce kernel entries from econstr.
Gaëtan Gilbert
2018-12-06
Evarutil.finalize: combine minimize, to_constr and restrict.
Gaëtan Gilbert
2018-12-06
Rename generated directory gramlib__pack -> gramlib/.pack
Gaëtan Gilbert
2018-12-06
unignore Makefile.install
Gaëtan Gilbert
2018-12-06
Fix race condition triggered by fresh universe generation
Maxime Dénès
2018-12-06
Merge PR #8917: Small cleanup wrt attributes_of_flags and template attribute
Vincent Laporte
2018-12-06
Merge pull request coq/ltac2#90 from ejgallego/tests
Pierre-Marie Pédrot
2018-12-06
Merge PR #9069: [gramlib] Remove dead code
Hugo Herbelin
2018-12-05
[ci] Add four color theorem proof to CI
Emilio Jesus Gallego Arias
2018-12-05
Remove the Like level modifier from gramlib.
Pierre-Marie Pédrot
2018-12-05
Remove the grammar-entry correspondence dynamic check in camlp5.
Pierre-Marie Pédrot
2018-12-05
Removing dead fields from Plexing.lexer.
Pierre-Marie Pédrot
2018-12-05
Remove dead code in camlp5.
Pierre-Marie Pédrot
2018-12-05
Remove the lexer field from Gramlib.
Pierre-Marie Pédrot
2018-12-05
Make some camlp5 fields immutable.
Pierre-Marie Pédrot
2018-12-05
Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`
Pierre-Marie Pédrot
2018-12-05
Merge pull request #20 from ejgallego/vernac+remove_empty_hooks
Emilio Jesús Gallego Arias
2018-12-05
Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.
Pierre-Marie Pédrot
2018-12-05
Move template out of Defattributes record
Gaëtan Gilbert
2018-12-05
attributes_of_flags and its output type now internal in vernacentries
Gaëtan Gilbert
2018-12-05
Add test for #8951.
Gaëtan Gilbert
2018-12-05
Fix mod_subst wrt universe polymorphism
Gaëtan Gilbert
2018-12-05
Merge PR #8911: Document undocumented flags and options
Théo Zimmermann
2018-12-04
Add undocumented options from mattam82
Jim Fehrle
2018-12-04
Document undocumented flags and options
Jim Fehrle
2018-12-04
Remove undocumented "Proof using Clear Unused" flag
Jim Fehrle
2018-12-04
Merge PR #9134: CI: track dev branch of coq-simple-io
Emilio Jesus Gallego Arias
2018-12-04
CI: track dev branch of coq-simple-io
Yishuai Li
2018-12-04
Merge PR #9127: Remove leftover code that used to handle ml4 files.
Emilio Jesus Gallego Arias
[prev]
[next]