| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-10 | CLEANUP: the definition of "type of constructor" was rephrased in order to ↵ | Matej Kosik | |
| make it more clear | |||
| 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 | FIX: commit 315f771 | Matej Kosik | |
| 2015-12-10 | CLEANUP: superfluous examples were removed | Matej Kosik | |
| 2015-12-10 | ENH: new example: "even" | Matej Kosik | |
| 2015-12-10 | ALPHA-CONVERSION: s/Length/has_length/g | Matej Kosik | |
| 2015-12-10 | ENH: examples | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: Examples of "arity" concept(s) were put to a separate ↵ | Matej Kosik | |
| \paragraph{...} | |||
| 2015-12-10 | ENH: adding a definition of the concept "_ is an arity". | Matej Kosik | |
| There already exists a definition of the following concept: "_ is an arity of sort _" I was not 100% sure what the following concept (used later in the text) means: "_ is an arity" so I added this (simple) definition in order to avoid possible confusion. | |||
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | CLEANUP: Presentation of examples was changed to make them more comprehensible. | Matej Kosik | |
| 2015-12-10 | SILENT: s/coq_example/coq_example*/ | Matej Kosik | |
| 2015-12-10 | QUESTION: Cannot we simplify the presentation of "Ind" and "Constr" typing ↵ | Matej Kosik | |
| rules like this? | |||
| 2015-12-10 | ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ↵ | Matej Kosik | |
| order to make it more concrete and more comprehensible. This ver | |||
| 2015-12-10 | ENH: the concept of 'inductive declaration' was added to the 'Global Index' | Matej Kosik | |
| 2015-12-10 | ENH: a small remark about Prod1 and Prod2 typing-rules was added | Matej Kosik | |
| 2015-12-10 | CLEANUP: the explanation of why eta-reduction is a bad idea was rephrased | Matej Kosik | |
| 2015-12-10 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: getting rid of an extra space | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: Each of the three 'Ax' and 'Prod' rules now has a unique name. | 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 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: removal of a definition of a concept that is not used ↵ | Matej Kosik | |
| further in the text | |||
| 2015-12-10 | ENH: 'Global Index' was enriched. | Matej Kosik | |
| These notions: - local assumption - local definition - global assumption - global definition are now indexed. | |||
| 2015-12-10 | SILENT: the anchor for the 'Local context' was moved to a more appropriate ↵ | Matej Kosik | |
| place. | |||
| 2015-12-10 | CLEANUP PROPOSITION: 'declaration' --> 'local declaration' | Matej Kosik | |
| If, below, we speak about 'global declarations', here it makes sense to speak about 'local declaration'. | |||
| 2015-12-10 | CLEANUP PROPOSITION: this sentence does not help us to better understand the ↵ | Matej Kosik | |
| semantics of the language | |||
| 2015-12-10 | CLEANUP PROPOSITION: The removed paragraph is not essential for this ↵ | Matej Kosik | |
| chapter. That kind of information is more appropriate for Section 1.2. | |||
| 2015-12-10 | TYPOGRAPHY: 'non dependent product', just like 'dependent product' is now ↵ | Matej Kosik | |
| emphasized | |||
| 2015-12-10 | ENH: a new anchor for an existing 'Global Index' keyword 'products' was added | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: The 'pCIC' keyword from the 'Global Index' was removed. | Matej Kosik | |
| We do not actually define the 'pCIC' concept in Chapter 4 so it does not make sense to keep an entry in the 'Global Index' for it. | |||
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | ENH: the concept of the 'algebraic universe' was added to the 'Global Index'. | Matej Kosik | |
| 2015-12-10 | ENH: Index anchor repositioning. | Matej Kosik | |
| Originally, when user clicked in index on "Type", he landed on an incorrect page (immediatelly following the page which actually contains the definition of "Type"). | |||
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: Duplicate information was removed and replaced with a ↵ | Matej Kosik | |
| reference to the corresponding section. | |||
| 2015-12-10 | ENH: citation | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: Duplicate information was removed and replaced with a ↵ | Matej Kosik | |
| reference to the corresponding chapter. | |||
| 2015-12-10 | Changing representation of prod over two Type: since the rule needs ↵ | Hugo Herbelin | |
| subtyping anyway to manage the Set and Prop cases, why not to simplify it by using subtyping also for managing Type. | |||
| 2015-12-10 | Removing note on shifting the hierarchy by 1 in 8.4, which makes things more ↵ | Hugo Herbelin | |
| complicated than needed. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |