| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2015-12-10 | Starting revising inductive types session | Hugo Herbelin | |
| 2015-12-10 | More consistency in the letter used to represent terms. | Hugo Herbelin | |
| + adding type of the defined term in let-in. | |||
| 2015-12-10 | More consistency in the names of inference rules. | Hugo Herbelin | |
| 2015-12-10 | Reformulating subtyping in a way closer to implementation. | Hugo Herbelin | |
| 2015-12-10 | fix | Hugo Herbelin | |
| 2015-12-10 | Smoothing the introduction and section Terms. | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Rephrasing and moving paragraph on the double reading | Hugo Herbelin | |
| proof/program of the syntax. | |||
| 2015-12-10 | RefMan, ch. 4: Misc. local improvements and typesetting. | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Removing the local context of inductive definitions. | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Adding discharging of inductive types. | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Moving section on discharge after inductive types. | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Avoiding using "inductive family" which is not defined. | Hugo Herbelin | |
| Using consistently "inductive types". | |||
| 2015-12-10 | RefMan, ch. 4: a few clarifications, thanks to Matej. | Hugo Herbelin | |
| There is still something buggy in explaining the interpretation of "match" as "case": we need typing to reconstruct the types of the x and y1..yn from the "as x in I ... y1..yn" clause. | |||
| 2015-12-10 | RefMan, ch. 4: Reference Manual: more on the "in pattern" clause and | Hugo Herbelin | |
| "@qualid pattern". | |||
| 2015-12-10 | RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local | Hugo Herbelin | |
| context for discharge in global declarations. Discharge now done on a global declaration. Hence removed Def and Assum which were only partially used (e.g. in rules Def and Assum but not in delta-conversion, nor in rule Const). Added discharge rule over definitions using let-in. It replaces the "substitution" rule since about 7.0. | |||
| 2015-12-10 | RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being | Hugo Herbelin | |
| clearer that the version depends on the version of Coq. Also renouncing to the "Predicative" and "(Co)" in the name, since after all, usage seems to continue calling the language of Coq Calculus of Inductive Constructions and to consider the Set predicative vs Set impredicative, as well as the presence of coinduction, as flavors of the CIC. | |||
| 2015-12-10 | RefMan, ch. 4: Dropping the "Co" which noone uses in "(Co)Inductive". | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions". | Hugo Herbelin | |
| 2015-12-10 | RefMan, ch. 4: Removing confusing paragraph "Constants": in it, | Hugo Herbelin | |
| constants are yet given another definition; the reference to other presentation is more confusing than helpful to me. | |||
| 2015-12-10 | RefMan, ch. 4: Consistently using "constant" for names assumed or defined | Hugo Herbelin | |
| in global environment and "variable" for names assumed or defined in local context. | |||
| 2015-12-10 | RefMan, ch. 4: Fixing the definition of terms considered in the section. | Hugo Herbelin | |
| 2015-12-09 | a few edits to the universe polymorphism section of the manual | Gregory Malecha | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |