aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* TYPOGRAPHY: Each of the three 'Ax' and 'Prod' rules now has a unique name.Gravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* TYPOGRAPHYGravatar Matej Kosik2015-12-10
* GRAMMARGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: removal of a definition of a concept that is not used fu...Gravatar Matej Kosik2015-12-10
* ENH: 'Global Index' was enriched.Gravatar Matej Kosik2015-12-10
* SILENT: the anchor for the 'Local context' was moved to a more appropriate pl...Gravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: 'declaration' --> 'local declaration'Gravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: this sentence does not help us to better understand the ...Gravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: The removed paragraph is not essential for this chapter....Gravatar Matej Kosik2015-12-10
* TYPOGRAPHY: 'non dependent product', just like 'dependent product' is now emp...Gravatar Matej Kosik2015-12-10
* ENH: a new anchor for an existing 'Global Index' keyword 'products' was addedGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* GRAMMARGravatar Matej Kosik2015-12-10
* COMMENT: questionGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: The 'pCIC' keyword from the 'Global Index' was removed.Gravatar Matej Kosik2015-12-10
* COMMENT: to doGravatar Matej Kosik2015-12-10
* ENH: the concept of the 'algebraic universe' was added to the 'Global Index'.Gravatar Matej Kosik2015-12-10
* ENH: Index anchor repositioning.Gravatar Matej Kosik2015-12-10
* COMMENT: to doGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: Duplicate information was removed and replaced with a re...Gravatar Matej Kosik2015-12-10
* ENH: citationGravatar Matej Kosik2015-12-10
* CLEANUP PROPOSITION: Duplicate information was removed and replaced with a re...Gravatar Matej Kosik2015-12-10
* Changing representation of prod over two Type: since the rule needs subtyping...Gravatar Hugo Herbelin2015-12-10
* Removing note on shifting the hierarchy by 1 in 8.4, which makes things more ...Gravatar Hugo Herbelin2015-12-10
* Starting revising inductive types sessionGravatar Hugo Herbelin2015-12-10
* More consistency in the letter used to represent terms.Gravatar Hugo Herbelin2015-12-10
* More consistency in the names of inference rules.Gravatar Hugo Herbelin2015-12-10
* Reformulating subtyping in a way closer to implementation.Gravatar Hugo Herbelin2015-12-10
* fixGravatar Hugo Herbelin2015-12-10
* Smoothing the introduction and section Terms.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Rephrasing and moving paragraph on the double readingGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Misc. local improvements and typesetting.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Removing the local context of inductive definitions.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Adding discharging of inductive types.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Moving section on discharge after inductive types.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Avoiding using "inductive family" which is not defined.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: a few clarifications, thanks to Matej.Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Reference Manual: more on the "in pattern" clause andGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a localGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Reformulating introduction of the chapter on CIC, beingGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Dropping the "Co" which noone uses in "(Co)Inductive".Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Unify capitalization of "calculus of inductive constructions".Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Removing confusing paragraph "Constants": in it,Gravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Consistently using "constant" for names assumed or definedGravatar Hugo Herbelin2015-12-10
* RefMan, ch. 4: Fixing the definition of terms considered in the section.Gravatar Hugo Herbelin2015-12-10
* Print Assumptions: improve detection of case on an axiom of FalseGravatar Enrico Tassi2015-12-09
* Remove remaining occurrences of Unix.readdir.Gravatar Guillaume Melquiond2015-12-09
* Replace Unix.readdir by Sys.readdir in dir cache.Gravatar Emilio Jesus Gallego Arias2015-12-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 10:39:36 +0000