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-01-29
Merge PR #9383: Remove travis
Vincent Laporte
2019-01-29
Merge PR #9424: Surround "assumption" with :tacn:`` in tactics.rst
Théo Zimmermann
2019-01-28
Surround "assumption" with :tacn:`` in tactics.rst
Ryan Scott
2019-01-28
Merge PR #9420: [doc] Remove emacs mentions from INSTALL
Théo Zimmermann
2019-01-28
[doc] Remove emacs mentions from INSTALL
Emilio Jesus Gallego Arias
2019-01-28
Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.
Théo Zimmermann
2019-01-28
Merge PR #9341: [ssr] uniform clear discipline
Maxime Dénès
2019-01-27
Merge PR #9399: [ide] fail on unavailable commands before adding to the document
Emilio Jesus Gallego Arias
2019-01-27
[test] for bug #9385
Enrico Tassi
2019-01-27
[fake_ide] infrastructure to test the failure of an ADD
Enrico Tassi
2019-01-27
[ide] fail on unavailable commands before adding to the document
Enrico Tassi
2019-01-27
Merge PR #9263: [STM] explicit handling of parsing states
Emilio Jesus Gallego Arias
2019-01-27
Merge PR #9214: Notations: Removing useless parentheses on abbreviations shor...
Emilio Jesus Gallego Arias
2019-01-25
Merge PR #9362: Fix makefile .merlin for unit tests
Enrico Tassi
2019-01-25
Merge PR #9391: Clarify meaning of Primitive Projections
Théo Zimmermann
2019-01-25
Merge PR #8637: Update -compat to support -compat 8.10
Théo Zimmermann
2019-01-25
Added a line about notation bug fixes.
Hugo Herbelin
2019-01-25
Notations: Removing useless parentheses on abbrevs for prefix of an application.
Hugo Herbelin
2019-01-24
Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].
Hugo Herbelin
2019-01-24
Update update-compat.py and release-process.md
Jason Gross
2019-01-24
Update -compat to support -compat 8.10
Jason Gross
2019-01-24
Update update-compat.py script
Jason Gross
2019-01-25
Move \def\plus and \def\tri to refman-preamble.sty.
Tanaka Akira
2019-01-24
Merge PR #9384: Improve the note in the beginning of the Ltac chapter.
Clément Pit-Claudel
2019-01-24
Add Overlays
Maxime Dénès
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2019-01-24
[STM] API to print a Stateid.t
Enrico Tassi
2019-01-24
Merge PR #9269: Move and rewrite intro pattern section
Théo Zimmermann
2019-01-24
Merge PR #9392: Fix small errors in cic.rst.
Théo Zimmermann
2019-01-24
Merge PR #9394: [nix-ci] Maintenance
Théo Zimmermann
2019-01-24
[nix-CI] Split the build inputs
Vincent Laporte
2019-01-24
[Nix-ci] Add QuickChick
Vincent Laporte
2019-01-24
[Nix-ci] Fix Unicoq
Vincent Laporte
2019-01-24
[Nix-ci] Add formal-topology
Vincent Laporte
2019-01-24
Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)
Matthieu Sozeau
2019-01-24
[doc] warn that (automatic) clears can result in errors
Enrico Tassi
2019-01-24
[doc] more precise description of when automatic clears are triggered
Enrico Tassi
2019-01-24
[doc] explain how to avoid automatic clears
Enrico Tassi
2019-01-24
Merge PR #9372: [thread] protect threads against sigalrm
Emilio Jesus Gallego Arias
2019-01-24
add comment
Enrico Tassi
2019-01-24
use \nO, \nS, etc. fix \kw{n}.
Tanaka Akira
2019-01-24
Fix small errors in cic.rst.
Tanaka Akira
2019-01-23
Clarify meaning of Primitive Projections
David A. Dalrymple
2019-01-23
Move and rewrite documentation for intro patterns that was under
Jim Fehrle
2019-01-23
Merge PR #9357: Fix recursive loadpath of ML files
Emilio Jesus Gallego Arias
2019-01-23
Merge PR #9043: [windows] Cleanup cruft from `dev/build/windows`
Michael Soegtrop
2019-01-23
Merge PR #9270: Turn `Refine instance Mode` off by default
Pierre-Marie Pédrot
2019-01-23
Merge PR #9374: Documentation: ring and field simplify can take no arguments
Théo Zimmermann
2019-01-23
Fix the information of the level of ; vs ; [ ]
Théo Zimmermann
2019-01-23
Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an...
Pierre-Marie Pédrot
[next]