index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
/
language
/
cic.rst
Age
Commit message (
Expand
)
Author
2019-03-14
Documentation for SProp
Gaëtan Gilbert
2019-02-20
Merge PR #9457: Correct W-Ind in Cic description of the reference manual.
Théo Zimmermann
2019-02-19
Make the conclusion of local contexts W-Ind empty.
Tanaka Akira
2019-02-13
Merge PR #9564: Fix small errors in cic.rst (3rd)
Théo Zimmermann
2019-02-12
Fix failing coqtops in cic.rst
Gaëtan Gilbert
2019-02-11
Use math mode more.
Tanaka Akira
2019-02-11
Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.
Tanaka Akira
2019-02-11
Remove a space before closing double-quote.
Tanaka Akira
2019-02-10
Change "I" to "I_p".
Tanaka Akira
2019-02-10
Distinguish inductive {definition,inductive}.
Tanaka Akira
2019-02-08
Use math mode more.
Tanaka Akira
2019-02-08
Fix index of arguments of constructor in fixpoint.
Tanaka Akira
2019-02-08
Change parameters p_1...p_r to q_1...q_r.
Tanaka Akira
2019-02-08
Change the index "p" to "s" in "type of branches".
Tanaka Akira
2019-02-08
Change c to c' forgotten at exchanging c and c'.
Tanaka Akira
2019-02-08
Remove spaces just before period (non-math mode).
Tanaka Akira
2019-02-08
Remove spaces just before comma (non-math mode).
Tanaka Akira
2019-02-08
Remove "'" accidentaly added.
Tanaka Akira
2019-02-01
Correct W-Ind.
Tanaka Akira
2019-02-01
The lowest universe level is 1.
Tanaka Akira
2019-01-31
Use λ instead of \lb.
Tanaka Akira
2019-01-31
The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.
Tanaka Akira
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-25
Move \def\plus and \def\tri to refman-preamble.sty.
Tanaka Akira
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-08
Add doc for auto-template warning
Gaëtan Gilbert
2018-10-29
Fix typos in the document about CIC
wkwkes
2018-10-23
Order Greek letters consistently w/rest of document
Sam Pablo Kuper
2018-09-20
Rewrite "Flags, Options and Tables" section.
Jim Fehrle
2018-09-20
[doc] Include the rst and LaTeX preambles automatically in all files
Clément Pit-Claudel
[next]