index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
/
RefMan-cic.tex
Commit message (
Expand
)
Author
Age
*
Rename \Tree to \NatTree
Johannes Kloos
2017-10-25
*
Fix #5763: Strictly positive example is out of order.
jkloos
2017-10-24
*
Avoid generated names for html pages of the reference manual (bug #4742).
Guillaume Melquiond
2017-09-22
*
Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style
Maxime Dénès
2017-08-16
|
\
|
*
Port ssr manual to Coq's latex/hevea style
Enrico Tassi
2017-08-02
*
|
Fix some coq-tex errors in the reference manual.
Guillaume Melquiond
2017-07-28
|
/
*
Document cumulativity for inductive types
Amin Timany
2017-06-16
*
refman: remember the old name of template polymorphism.
Gaetan Gilbert
2017-04-24
*
Use "template polymorphism" in the documentation.
Gaetan Gilbert
2017-04-11
*
Mention template polymorphism in the documentation.
Gaetan Gilbert
2017-04-11
*
FIX: HTML version of Chapter 4 of the Reference Manual
Matej Kosik
2016-04-12
*
TYPOGRAPHY: adding missing \noindent macros
Matej Kosik
2016-04-12
*
Fix \label which was meants to be \ref in doc of CIC terms.
Maxime Dénès
2015-12-14
*
Refman, ch. 4: A few fixes.
Hugo Herbelin
2015-12-10
*
ENH: redundant examples were removed
Matej Kosik
2015-12-10
*
FIX: wrong reference to a figure
Matej Kosik
2015-12-10
*
CLEANUP: putting examples inside "figure" environment
Matej Kosik
2015-12-10
*
ENH: The definition of the "_ ; _" operation on local context was added.
Matej Kosik
2015-12-10
*
TYPOGRAPHY: adjustments
Matej Kosik
2015-12-10
*
PROPOSITION: the side-condition was made more specific.
Matej Kosik
2015-12-10
*
PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'
Matej Kosik
2015-12-10
*
PROPOSITION: Added an explicit definition of the notation for enriching the g...
Matej Kosik
2015-12-10
*
PROPOSITION: Added "if" and "then" words missing in the original sentence.
Matej Kosik
2015-12-10
*
PROPOSITION: Example was simplified
Matej Kosik
2015-12-10
*
DONE
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
COMMENT: question
Matej Kosik
2015-12-10
*
TYPOGRAPHY
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
*
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
[next]