| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond | |
| 2015-12-06 | RefMan, ch. 1 and 2: avoiding using the name "constant" when | Hugo Herbelin | |
| "constructor" and "inductive" are meant also. | |||
| 2015-12-06 | RefMan, ch. 4: Consistent use of the terms local context and global environment. | Hugo Herbelin | |
| 2015-12-06 | RefMan, ch. 4: Terminology constant/names. | Hugo Herbelin | |
| 2015-12-06 | RefMan, ch. 4: Minor changes for spacing, clarity. | Hugo Herbelin | |
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-02 | Improving syntax of pat/constr introduction pattern so that | Hugo Herbelin | |
| pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though. | |||
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-26 | Adding the Printing Projections options to the index. | Pierre-Marie Pédrot | |
| 2015-11-07 | Fixing documention of Add Printing Coercion. | Hugo Herbelin | |
| 2015-11-04 | Univs: update refman, better printers for universe contexts. | Matthieu Sozeau | |
| 2015-11-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin | |
| starting a sentence with a symbolic expression. | |||
| 2015-10-14 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-11 | Documenting matching under binders. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |