index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
refman
Age
Commit message (
Expand
)
Author
2015-12-10
ENH: improving precision
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
FIX: "u_p" was not defined
Matej Kosik
2015-12-10
CLEANUP: removing duplicate paragraph
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: questions and to do
Matej Kosik
2015-12-10
FIX: removing references to Γ which is not defined in a given context
Matej Kosik
2015-12-10
TYPESETTING
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
GRAMMAR
Matej Kosik
2015-12-10
CLEANUP PROPOSITION: superfluous parentheses were removed
Matej Kosik
2015-12-10
CLEANUP PROPOSITION: s/local context of parameters/context of parameters
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: questions
Matej Kosik
2015-12-10
COMMENT: to do
Matej Kosik
2015-12-10
COMMENT: to do
Matej Kosik
2015-12-10
FIX: removing a reference to \Gamma, because it is undefined
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
FIX: making sure that my previous edits do not break HTML generation
Matej Kosik
2015-12-10
COMMENT: questions
Matej Kosik
2015-12-10
ENH: examples for 'strict positivity' were expanded
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
CLEANUP: the definition of "type of constructor" was rephrased in order to ma...
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
COMMENT: to do
Matej Kosik
2015-12-10
FIX: commit 315f771
Matej Kosik
2015-12-10
CLEANUP: superfluous examples were removed
Matej Kosik
2015-12-10
ENH: new example: "even"
Matej Kosik
2015-12-10
ALPHA-CONVERSION: s/Length/has_length/g
Matej Kosik
2015-12-10
ENH: examples
Matej Kosik
2015-12-10
TYPOGRAPHY: Examples of "arity" concept(s) were put to a separate \paragraph{...
Matej Kosik
2015-12-10
ENH: adding a definition of the concept "_ is an arity".
Matej Kosik
2015-12-10
TYPOGRAPHY
Matej Kosik
2015-12-10
TYPOGRAPHY
Matej Kosik
2015-12-10
COMMENT: to do
Matej Kosik
2015-12-10
CLEANUP: Presentation of examples was changed to make them more comprehensible.
Matej Kosik
2015-12-10
SILENT: s/coq_example/coq_example*/
Matej Kosik
2015-12-10
QUESTION: Cannot we simplify the presentation of "Ind" and "Constr" typing ru...
Matej Kosik
2015-12-10
ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord...
Matej Kosik
2015-12-10
ENH: the concept of 'inductive declaration' was added to the 'Global Index'
Matej Kosik
2015-12-10
ENH: a small remark about Prod1 and Prod2 typing-rules was added
Matej Kosik
2015-12-10
CLEANUP: the explanation of why eta-reduction is a bad idea was rephrased
Matej Kosik
2015-12-10
GRAMMAR
Matej Kosik
2015-12-10
TYPOGRAPHY: getting rid of an extra space
Matej Kosik
2015-12-10
COMMENT: question
Matej Kosik
2015-12-10
TYPOGRAPHY: Each of the three 'Ax' and 'Prod' rules now has a unique name.
Matej Kosik
[prev]
[next]