| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Print Assumptions: improve detection of case on an axiom of False | Enrico Tassi | |
| The name in the return clause has no semantic meaning, we must not look at it. | |||
| 2015-12-09 | Remove remaining occurrences of Unix.readdir. | Guillaume Melquiond | |
| 2015-12-09 | Replace Unix.readdir by Sys.readdir in dir cache. | Emilio Jesus Gallego Arias | |
| This makes the function sightly more portable. | |||
| 2015-12-09 | a few edits to the universe polymorphism section of the manual | Gregory Malecha | |
| 2015-12-09 | bug fixes to vm computation + test cases. | Gregory Malecha | |
| 2015-12-09 | The unshelve tactical now takes future goals into account. | Pierre-Marie Pédrot | |
| 2015-12-09 | Fixing parsing of the unshelve tactical. | Pierre-Marie Pédrot | |
| Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2]. | |||
| 2015-12-09 | Adding an unshelve tactical. | Pierre-Marie Pédrot | |
| This tactical is inspired by discussions on the Coq-club list. For now it is still undocumented, and there is room left for design issues. | |||
| 2015-12-07 | Fixing a minor problem in Makefile.build that was prevening ↵ | Matej Kosik | |
| "dev/printers.cma" to be loadable within "ocamldebug". | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |