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-02-28
Merge PR #6853: Add a comment on EConstr.to_constr regarding evar-freeness.
Maxime Dénès
2018-02-28
Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas
Maxime Dénès
2018-02-28
Merge PR #6756: Fix issue with spurious timing test failures
Maxime Dénès
2018-02-28
Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...
Maxime Dénès
2018-02-28
Merge PR #6789: Check whitespace errors per-commit.
Maxime Dénès
2018-02-28
Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)
Maxime Dénès
2018-02-28
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...
Maxime Dénès
2018-02-28
Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...
Maxime Dénès
2018-02-28
Merge PR #6752: Remove from CircleCI builds that are already taken care of by...
Maxime Dénès
2018-02-28
Remove empty, wrongly located, doc file.
Théo Zimmermann
2018-02-27
Typo in the documentation of the `pattern` tactic
Joachim Breitner
2018-02-27
comment "resolvability" bit in Evd.evar_map
Enrico Tassi
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-27
Fix #6751 trust_file_cache logic was inverted
Gaëtan Gilbert
2018-02-27
Add a comment on EConstr.to_constr regarding evar-freeness.
Pierre-Marie Pédrot
2018-02-27
Merge remote-tracking branch 'origin/pr/44'
Pierre-Marie Pédrot
2018-02-27
[stdlib] move “Require” out of sections
Vincent Laporte
2018-02-27
Use relative path for show_latex_messages
mrmr1993
2018-02-27
Use MYCAMLP5LIB instead of undefined MYCAMLP4LIB
mrmr1993
2018-02-24
Add String.concat
Jason Gross
2018-02-24
[test-suite] Move sed scripts into bash arrays
Jason Gross
2018-02-24
Merge PR #6543: Update headers and credits
Maxime Dénès
2018-02-24
Merge PR #6784: New IR in VM: Clambda
Maxime Dénès
2018-02-24
Merge PR #6819: Document Arguments extra scopes flag
Maxime Dénès
2018-02-24
Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).
Maxime Dénès
2018-02-24
Merge PR #6803: coqdev.el: add space at the end of compile-command
Maxime Dénès
2018-02-24
Merge PR #6599: Decimals in prelude
Maxime Dénès
2018-02-24
Merge PR #6745: [ast] Improve precision of Ast location recognition in serial...
Maxime Dénès
2018-02-23
Check whitespace errors per-commit.
Gaëtan Gilbert
2018-02-23
New IR in VM: Clambda.
Maxime Dénès
2018-02-23
Fix map iterator on nativelambda.
Maxime Dénès
2018-02-23
Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).
Hugo Herbelin
2018-02-22
Document Arguments extra scopes flag
Jasper Hugunin
2018-02-22
Tweak developer documentation.
Jim Fehrle
2018-02-22
Rename release_lexer_state to the more descriptive get_lexer_state.
Jim Fehrle
2018-02-22
Adding mention of shelved/given-up status in "Show Existentials".
Hugo Herbelin
2018-02-22
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-21
Remove from CircleCI builds that are already taken care of by Travis.
Théo Zimmermann
2018-02-21
Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`
Maxime Dénès
2018-02-21
Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred
Maxime Dénès
2018-02-21
Merge PR #6767: [ci] add elpi
Maxime Dénès
2018-02-21
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Maxime Dénès
2018-02-21
Merge PR #6283: A pre-commit hook to magically fix whitespace issues.
Maxime Dénès
2018-02-21
Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just the...
Maxime Dénès
2018-02-21
Merge PR #6740: Adding a sanity check on inductive variance subtyping.
Maxime Dénès
2018-02-21
Update CREDITS.
Théo Zimmermann
2018-02-21
More accurate and complete headers.
Théo Zimmermann
2018-02-21
Mention the CREDITS file in CONTRIBUTING.
Théo Zimmermann
2018-02-21
Remove redundant COPYRIGHT file.
Théo Zimmermann
2018-02-21
coqdev.el: add space at the end of compile-command
Gaëtan Gilbert
[prev]
[next]