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-31
Don't line break at hyphen of compound words.
Tanaka Akira
2019-01-31
Move out a period and comma from :math:.
Tanaka Akira
2019-01-31
Nest :math: and parenthesis properly.
Tanaka Akira
2019-01-31
Fix syntax of two lambda-abstractions.
Tanaka Akira
2019-01-31
Change {\Sort} to \Sort.
Tanaka Akira
2019-01-31
Use \Prop, \Set and \Type defined in refman-preamble.sty.
Tanaka Akira
2019-01-31
Make "1" and "2" in "f1" and "f2" suffixes.
Tanaka Akira
2019-01-31
Make "1" and "n" in "u1" and "un" suffixes.
Tanaka Akira
2019-01-31
Remove "End TreeExample." line.
Tanaka Akira
2019-01-31
Merge PR #8720: [Numeral notations] Use Coqlib registered constants
Emilio Jesus Gallego Arias
2019-01-30
Merge PR #9440: Create deployment environment for Cachix.
Emilio Jesus Gallego Arias
2019-01-30
Create deployment environment for Cachix.
Théo Zimmermann
2019-01-29
Merge PR #9417: Update update-compat.py script
Théo Zimmermann
2019-01-29
Merge PR #9435: Use \mathcal instead of \cal
Théo Zimmermann
2019-01-29
Update update-compat.py script
Jason Gross
2019-01-29
Merge PR #9274: Make `Instance` without a body always open a proof
Enrico Tassi
2019-01-29
Use \mathcal instead of \cal
Gaëtan Gilbert
2019-01-29
Merge PR #9421: [vernac] Fix classification of `Declare Custom Entry`
Enrico Tassi
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
[vernac] Fix classification of `Declare Custom Entry`
Emilio Jesus Gallego Arias
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-25
[Numeral notations] Lazy resolution of decimal types
Vincent Laporte
2019-01-25
[Numeral notations] Use Coqlib registered constants
Vincent Laporte
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
Make `Instance` without a body always open a proof.
Maxime Dénès
2019-01-24
Merge PR #9269: Move and rewrite intro pattern section
Théo Zimmermann
[next]