aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-cic.tex
AgeCommit message (Expand)Author
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
2015-12-10Starting revising inductive types sessionHugo Herbelin
2015-12-10More consistency in the letter used to represent terms.Hugo Herbelin
2015-12-10More consistency in the names of inference rules.Hugo Herbelin
2015-12-10Reformulating subtyping in a way closer to implementation.Hugo Herbelin
2015-12-10fixHugo Herbelin
2015-12-10Smoothing the introduction and section Terms.Hugo Herbelin
2015-12-10RefMan, ch. 4: Rephrasing and moving paragraph on the double readingHugo Herbelin
2015-12-10RefMan, ch. 4: Misc. local improvements and typesetting.Hugo Herbelin
2015-12-10RefMan, ch. 4: Removing the local context of inductive definitions.Hugo Herbelin
2015-12-10RefMan, ch. 4: Adding discharging of inductive types.Hugo Herbelin
2015-12-10RefMan, ch. 4: Moving section on discharge after inductive types.Hugo Herbelin
2015-12-10RefMan, ch. 4: Avoiding using "inductive family" which is not defined.Hugo Herbelin
2015-12-10RefMan, ch. 4: a few clarifications, thanks to Matej.Hugo Herbelin
2015-12-10RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a localHugo Herbelin
2015-12-10RefMan, ch. 4: Reformulating introduction of the chapter on CIC, beingHugo Herbelin
2015-12-10RefMan, ch. 4: Dropping the "Co" which noone uses in "(Co)Inductive".Hugo Herbelin
2015-12-10RefMan, ch. 4: Removing confusing paragraph "Constants": in it,Hugo Herbelin
2015-12-10RefMan, ch. 4: Consistently using "constant" for names assumed or definedHugo Herbelin
2015-12-10RefMan, ch. 4: Fixing the definition of terms considered in the section.Hugo Herbelin
2015-12-06RefMan, ch. 4: Consistent use of the terms local context and global environment.Hugo Herbelin
2015-12-06RefMan, ch. 4: Terminology constant/names.Hugo Herbelin
2015-12-06RefMan, ch. 4: Minor changes for spacing, clarity.Hugo Herbelin
2015-03-05Preprend Fail to all the expected failures in the documentation.Guillaume Melquiond
2014-12-09refman: switch all source files to utf8Pierre Letouzey
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-05Chapter 4 of reference manual: Fixing asymmetric patterns error +Hugo Herbelin
2014-08-03Chapter 4: Fixing ambiguity about whether the return predicate refersHugo Herbelin
2012-08-08Documenting eta-conversion.herbelin
2012-08-08More standard layout for \lambda in chapter CIC.herbelin
2012-05-08Rephrasing section on Sorts in CIC chapter, accordingly to discussionsherbelin
2012-05-08Ref. man., ch. CIC: clarifying the redundancy coming from having bothherbelin
2012-04-13Uniformisation in the documentation: remove the use of 'coinductive' inaspiwack
2010-05-28Minor fix in doc chapter on inference rules (added a missing space).herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-26Correction du bug #2214 + maj liens webnotin
2009-10-28Typo in the refmanpuech
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
2008-07-23Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theherbelin