| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-26 | Adding the Printing Projections options to the index. | Pierre-Marie Pédrot | |
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin | |
| Did some manual merge in tactics/tactics.ml. | |||
| 2015-11-07 | Adding an amazing property of Prop. | Hugo Herbelin | |
| 2015-11-07 | Fixing documention of Add Printing Coercion. | Hugo Herbelin | |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin | |
| starting a sentence with a symbolic expression. | |||
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-14 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-11 | Documenting matching under binders. | Hugo Herbelin | |
| 2015-10-10 | Fix a few latex errors in documentation of Proof Using (e.g. \tt*). | Guillaume Melquiond | |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | |
| - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |