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
Use "U" instead of "u" for a type.
Tanaka Akira
2019-01-31
Fix an index. The number of constructors is "l".
Tanaka Akira
2019-01-31
Use \Match for match construct.
Tanaka Akira
2019-01-31
Insert a space before \kwend.
Tanaka Akira
2019-01-31
Use \length for the function name of length.
Tanaka Akira
2019-01-31
Adjust spaces.
Tanaka Akira
2019-01-31
Use "∀" and "λ" instead of \forall and \lambda.
Tanaka Akira
2019-01-31
Use math more.
Tanaka Akira
2019-01-31
Make parenthesis correctly matched.
Tanaka Akira
2019-01-31
\Sort is not a term.
Tanaka Akira
2019-01-31
Use semicolon for separator of local contexts.
Tanaka Akira
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
[next]