| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-07 | Fixing a minor problem in Makefile.build that was prevening ↵ | Matej Kosik | |
| "dev/printers.cma" to be loadable within "ocamldebug". | |||
| 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 | Fixing compilation with old CAMLPX versions. | Pierre-Marie Pédrot | |
| 2015-12-05 | Factorizing unsafe code by relying on the new Dyn module. | Pierre-Marie Pédrot | |
| 2015-12-05 | Leveraging GADTs to provide a better Dyn API. | Pierre-Marie Pédrot | |
| 2015-12-05 | Making output of target source-doc a bit less verbose. | Hugo Herbelin | |
| 2015-12-05 | Fixing compilation of mli documentation. | Hugo Herbelin | |
| Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed. | |||
| 2015-12-05 | Fix to previous commit (ClassicalFacts.v). | Hugo Herbelin | |
| 2015-12-05 | Adding proofs on the relation between excluded-middle and minimization. | Hugo Herbelin | |
| In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs. | |||
| 2015-12-05 | Removing redundant versions of generalize. | Hugo Herbelin | |
| 2015-12-05 | Unifying betazeta_applist and prod_applist into a clearer interface. | Hugo Herbelin | |
| - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. | |||
| 2015-12-05 | Slight simplification of the code of primitive projection (in relation | Hugo Herbelin | |
| to c71aa6b and 6ababf) so as to rely on generic functions rather than re-doing the de Bruijn indices cooking locally. | |||
| 2015-12-05 | Moving extended_rel_vect/extended_rel_list to the kernel. | Hugo Herbelin | |
| It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. | |||
| 2015-12-05 | Simplifying an instantiation function using subst_of_rel_context_instance. | Hugo Herbelin | |
| 2015-12-05 | About building of substitutions from instances. | Hugo Herbelin | |
| Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. | |||
| 2015-12-05 | Experimenting documentation of the Vars.subst functions. | Hugo Herbelin | |
| Related questions: - What balance to find between precision and conciseness? - What convention to follow for typesetting the different components of the documentation is unclear? New tentative type substl to emphasize that substitutions (for substl) are represented the other way round compared to instances for application (applist), though there are represented the same way (i.e. most recent/dependent component on top) as instances of evars (mkEvar). Also removing unused subst*_named_decl functions (at least substnl_named_decl is somehow non-sense). | |||
| 2015-12-05 | Contracting one extra beta-redex on the fly when typing branches of "match". | Hugo Herbelin | |
| 2015-12-05 | A few renaming and simplification in inductive.ml. | Hugo Herbelin | |
| 2015-12-05 | Experimenting removing strong normalization of the mid-statement in tactic cut. | Hugo Herbelin | |
| 2015-12-05 | Moving three related small half-general half-ad-hoc utility functions | Hugo Herbelin | |
| next to each other, waiting for possible integration into a more uniform API. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |