aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-cic.tex
Commit message (Expand)AuthorAge
* Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
* refman: remember the old name of template polymorphism.Gravatar Gaetan Gilbert2017-04-24
* Use "template polymorphism" in the documentation.Gravatar Gaetan Gilbert2017-04-11
* Mention template polymorphism in the documentation.Gravatar Gaetan Gilbert2017-04-11
* FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
* TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
* Fix \label which was meants to be \ref in doc of CIC terms.Gravatar Maxime Dénès2015-12-14
* Refman, ch. 4: A few fixes.Gravatar Hugo Herbelin2015-12-10
* ENH: redundant examples were removedGravatar Matej Kosik2015-12-10
* FIX: wrong reference to a figureGravatar Matej Kosik2015-12-10
* CLEANUP: putting examples inside "figure" environmentGravatar Matej Kosik2015-12-10
* ENH: The definition of the "_ ; _" operation on local context was added.Gravatar Matej Kosik2015-12-10
* TYPOGRAPHY: adjustmentsGravatar Matej Kosik2015-12-10
* PROPOSITION: the side-condition was made more specific.Gravatar Matej Kosik2015-12-10
* PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added an explicit definition of the notation for enriching the g...Gravatar Matej Kosik2015-12-10
* PROPOSITION: Added "if" and "then" words missing in the original sentence.Gravatar Matej Kosik2015-12-10
* PROPOSITION: Example was simplifiedGravatar Matej Kosik2015-12-10
* DONEGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* TYPOGRAPHYGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: to doGravatar Matej Kosik2015-12-10
* GRAMMAR: added punctuationGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: rephrasing the original idea in a simpler wayGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: existing example was removed because it is not urgently ...Gravatar Matej Kosik2015-12-10
* ENH: existing example was changed so that it is now linked to the results sho...Gravatar Matej Kosik2015-12-10
* ENH: an existing example was further expanded.Gravatar Matej Kosik2015-12-10
* CLEANUP: Existing example was removed.Gravatar Matej Kosik2015-12-10
* ENH: existing example was expandedGravatar Matej Kosik2015-12-10
* ENH: define the meaning of 'p'Gravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...Gravatar Matej Kosik2015-12-10
* CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...Gravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* CLEANUP: removing a superfluous indexGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* GRAMMARGravatar Matej Kosik2015-12-10
* COMMENT: noteGravatar Matej Kosik2015-12-10
* TYPOGRAPHYGravatar Matej Kosik2015-12-10
* CLEANUP: originally, we talked about "B" as an "arity"Gravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* ENH: a forward reference to a place where the concept of "allowed elimination...Gravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* CLEANUP: unnecessaryGravatar Matej Kosik2015-12-10
* GRAMMARGravatar Matej Kosik2015-12-10