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-03-31
Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text
Pierre-Marie Pédrot
2019-03-31
Merge PR #8829: Error when [foo.(bar)] is used with nonprojection [bar], warn...
Pierre-Marie Pédrot
2019-03-31
[coq] Adapt to coq/coq#9815
Pierre Roux
2019-03-31
Revert "iconv bedrock2 CI output to UTF-8"
Jason Gross
2019-03-31
[pretty-timing scripts] Don't barf on non-utf-8
Jason Gross
2019-03-31
CI: add mit-pdos/argosy
Tej Chajed
2019-03-31
overlay for PR 9733
Enrico Tassi
2019-03-31
[pretty-print py]Don't print sys.stdout;better utf
Jason Gross
2019-03-31
documentation
Enrico Tassi
2019-03-31
overlay for ltac2
Enrico Tassi
2019-03-31
[parsing] add keyword-protected generic quotation
Enrico Tassi
2019-03-31
[parsing] Split Tok.t into Tok.t and Tok.pattern
Enrico Tassi
2019-03-31
[dune] typo
Enrico Tassi
2019-03-31
Merge PR #9841: Remove some [let foo = foo] in eqschemes
Pierre-Marie Pédrot
2019-03-31
Move content of COMPATIBILITY to Changes chapter.
Théo Zimmermann
2019-03-31
Move V8 CHANGES to Changes chapter.
Théo Zimmermann
2019-03-31
Move V7 CHANGES to History chapter.
Théo Zimmermann
2019-03-31
Change main sections in history chapter.
Théo Zimmermann
2019-03-31
Split credits chapter in two parts: history, and changelog in inverse chronol...
Théo Zimmermann
2019-03-31
Merge PR #9800: Less conv_tab allocations when pushing relevances, esp skip_p...
Pierre-Marie Pédrot
2019-03-30
Error when [foo.(bar)] is used with nonprojection [bar]
Gaëtan Gilbert
2019-03-30
Merge PR #8730: Add unicode category LM
Pierre-Marie Pédrot
2019-03-30
Merge pull request coq/ltac2#86 from ejgallego/more-dune
Pierre-Marie Pédrot
2019-03-30
[vernac] Small cleanup to remove assert false.
Emilio Jesus Gallego Arias
2019-03-30
[program] Allow evars in type of fixpoints.
Emilio Jesus Gallego Arias
2019-03-30
Overlay for Elpi
Vincent Laporte
2019-03-30
[Canonical structures] Minor refactoring
Vincent Laporte
2019-03-30
[Canonical structures] Minor cleaning
Vincent Laporte
2019-03-30
[Manual] Typo
Vincent Laporte
2019-03-30
Merge PR #9869: [CI] Force caching when running test-suite in async mode
Emilio Jesus Gallego Arias
2019-03-29
Merge PR #9858: Fix top_printers after removal of imperative state
Emilio Jesus Gallego Arias
2019-03-29
Merge PR #9830: [parser] initialization based on Loc.t rather than Loc.source
Emilio Jesus Gallego Arias
2019-03-29
[CI] Force caching when running test-suite in async mode
Maxime Dénès
2019-03-29
Merge PR #9866: typo in ring.rst
Théo Zimmermann
2019-03-29
Merge PR #9860: [dune] Fix shim quoting and add coqc wrapper.
Théo Zimmermann
2019-03-29
Merge PR #9859: [dune] Don't regenerate ltac/dune after bootstrapping.
Théo Zimmermann
2019-03-29
Merge PR #9853: Use only lowercase for unimath in CI scripts
Emilio Jesus Gallego Arias
2019-03-29
typo in ring.rst
thery
2019-03-29
[parser] initialization based on Loc.t rather than Loc.source
Enrico Tassi
2019-03-29
[dune] Full Dune support.
Emilio Jesus Gallego Arias
2019-03-29
Merge PR #9834: Ignore generated files for CoqIDE bindings
Gaëtan Gilbert
2019-03-28
Merge pull request coq/ltac2#109 from ejgallego/proof+no_global_partial
Pierre-Marie Pédrot
2019-03-28
[dune] Fix shim quoting and add coqc wrapper.
Emilio Jesus Gallego Arias
2019-03-28
[dune] Don't regenerate ltac/dune after bootstrapping.
Emilio Jesus Gallego Arias
2019-03-28
Fix top_printers after removal of imperative state
Gaëtan Gilbert
2019-03-28
Use only lowercase for unimath in CI scripts
Gaëtan Gilbert
2019-03-28
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers o...
Maxime Dénès
2019-03-28
Merge PR #9743: Relax the ambiguous path condition of coercion
Enrico Tassi
2019-03-28
Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`
Théo Zimmermann
2019-03-27
Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.
Jim Fehrle
[prev]
[next]