aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-cic.tex
AgeCommit message (Expand)Author
2018-03-15[Sphinx] Move chapter 4 to new infrastructureMaxime Dénès
2017-10-25Rename \Tree to \NatTreeJohannes Kloos
2017-10-24Fix #5763: Strictly positive example is out of order.jkloos
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-08-16Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleMaxime Dénès
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-07-28Fix some coq-tex errors in the reference manual.Guillaume Melquiond
2017-06-16Document cumulativity for inductive typesAmin Timany
2017-04-24refman: remember the old name of template polymorphism.Gaetan Gilbert
2017-04-11Use "template polymorphism" in the documentation.Gaetan Gilbert
2017-04-11Mention template polymorphism in the documentation.Gaetan Gilbert
2016-04-12FIX: HTML version of Chapter 4 of the Reference ManualMatej Kosik
2016-04-12TYPOGRAPHY: adding missing \noindent macrosMatej Kosik
2015-12-14Fix \label which was meants to be \ref in doc of CIC terms.Maxime Dénès
2015-12-10Refman, ch. 4: A few fixes.Hugo Herbelin
2015-12-10ENH: redundant examples were removedMatej Kosik
2015-12-10FIX: wrong reference to a figureMatej Kosik
2015-12-10CLEANUP: putting examples inside "figure" environmentMatej Kosik
2015-12-10ENH: The definition of the "_ ; _" operation on local context was added.Matej Kosik
2015-12-10TYPOGRAPHY: adjustmentsMatej Kosik
2015-12-10PROPOSITION: the side-condition was made more specific.Matej Kosik
2015-12-10PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'Matej Kosik
2015-12-10PROPOSITION: Added an explicit definition of the notation for enriching the g...Matej Kosik
2015-12-10PROPOSITION: Added "if" and "then" words missing in the original sentence.Matej Kosik
2015-12-10PROPOSITION: Example was simplifiedMatej Kosik
2015-12-10DONEMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10GRAMMAR: added punctuationMatej Kosik
2015-12-10CLEANUP PROPOSITION: rephrasing the original idea in a simpler wayMatej Kosik
2015-12-10CLEANUP PROPOSITION: existing example was removed because it is not urgently ...Matej Kosik
2015-12-10ENH: existing example was changed so that it is now linked to the results sho...Matej Kosik
2015-12-10ENH: an existing example was further expanded.Matej Kosik
2015-12-10CLEANUP: Existing example was removed.Matej Kosik
2015-12-10ENH: existing example was expandedMatej Kosik
2015-12-10ENH: define the meaning of 'p'Matej Kosik
2015-12-10CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive definit...Matej Kosik
2015-12-10CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive de...Matej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10CLEANUP: removing a superfluous indexMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10COMMENT: noteMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:33:48 +0000