aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2015-12-10CLEANUP: the definition of "type of constructor" was rephrased in order to ma...Matej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10FIX: commit 315f771Matej Kosik
2015-12-10CLEANUP: superfluous examples were removedMatej Kosik
2015-12-10ENH: new example: "even"Matej Kosik
2015-12-10ALPHA-CONVERSION: s/Length/has_length/gMatej Kosik
2015-12-10ENH: examplesMatej Kosik
2015-12-10TYPOGRAPHY: Examples of "arity" concept(s) were put to a separate \paragraph{...Matej Kosik
2015-12-10ENH: adding a definition of the concept "_ is an arity".Matej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10CLEANUP: Presentation of examples was changed to make them more comprehensible.Matej Kosik
2015-12-10SILENT: s/coq_example/coq_example*/Matej Kosik
2015-12-10QUESTION: Cannot we simplify the presentation of "Ind" and "Constr" typing ru...Matej Kosik
2015-12-10ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord...Matej Kosik
2015-12-10ENH: the concept of 'inductive declaration' was added to the 'Global Index'Matej Kosik
2015-12-10ENH: a small remark about Prod1 and Prod2 typing-rules was addedMatej Kosik
2015-12-10CLEANUP: the explanation of why eta-reduction is a bad idea was rephrasedMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10TYPOGRAPHY: getting rid of an extra spaceMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10TYPOGRAPHY: Each of the three 'Ax' and 'Prod' rules now has a unique name.Matej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10CLEANUP PROPOSITION: removal of a definition of a concept that is not used fu...Matej Kosik
2015-12-10ENH: 'Global Index' was enriched.Matej Kosik
2015-12-10SILENT: the anchor for the 'Local context' was moved to a more appropriate pl...Matej Kosik
2015-12-10CLEANUP PROPOSITION: 'declaration' --> 'local declaration'Matej Kosik
2015-12-10CLEANUP PROPOSITION: this sentence does not help us to better understand the ...Matej Kosik
2015-12-10CLEANUP PROPOSITION: The removed paragraph is not essential for this chapter....Matej Kosik
2015-12-10TYPOGRAPHY: 'non dependent product', just like 'dependent product' is now emp...Matej Kosik
2015-12-10ENH: a new anchor for an existing 'Global Index' keyword 'products' was addedMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10CLEANUP PROPOSITION: The 'pCIC' keyword from the 'Global Index' was removed.Matej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10ENH: the concept of the 'algebraic universe' was added to the 'Global Index'.Matej Kosik
2015-12-10ENH: Index anchor repositioning.Matej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10CLEANUP PROPOSITION: Duplicate information was removed and replaced with a re...Matej Kosik
2015-12-10ENH: citationMatej Kosik
2015-12-10CLEANUP PROPOSITION: Duplicate information was removed and replaced with a re...Matej Kosik
2015-12-10Changing representation of prod over two Type: since the rule needs subtyping...Hugo Herbelin
2015-12-10Removing note on shifting the hierarchy by 1 in 8.4, which makes things more ...Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 02:42:25 +0000