index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
...
|
*
GRAMMAR: added punctuation
Matej Kosik
2015-12-10
|
*
CLEANUP PROPOSITION: rephrasing the original idea in a simpler way
Matej Kosik
2015-12-10
|
*
CLEANUP PROPOSITION: existing example was removed because it is not urgently ...
Matej Kosik
2015-12-10
|
*
ENH: existing example was changed so that it is now linked to the results sho...
Matej Kosik
2015-12-10
|
*
ENH: an existing example was further expanded.
Matej Kosik
2015-12-10
|
*
CLEANUP: Existing example was removed.
Matej Kosik
2015-12-10
|
*
ENH: existing example was expanded
Matej Kosik
2015-12-10
|
*
ENH: define the meaning of 'p'
Matej Kosik
2015-12-10
|
*
CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...
Matej Kosik
2015-12-10
|
*
CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
|
*
CLEANUP: removing a superfluous index
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
|
*
GRAMMAR
Matej Kosik
2015-12-10
|
*
COMMENT: note
Matej Kosik
2015-12-10
|
*
TYPOGRAPHY
Matej Kosik
2015-12-10
|
*
CLEANUP: originally, we talked about "B" as an "arity"
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
|
*
ENH: a forward reference to a place where the concept of "allowed elimination...
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
|
*
CLEANUP: unnecessary
Matej Kosik
2015-12-10
|
*
GRAMMAR
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
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
|
*
CLEANUP: s/List_A/List~A/g
Matej Kosik
2015-12-10
|
*
COMMENT: question
Matej Kosik
2015-12-10
[prev]
[next]