| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2015-12-05 | An example in centralizing similar functions to a common place so that | Hugo Herbelin | |
| cleaning the interfaces is eventually easier. Here, adding find_mrectype_vect to simplify vnorm.ml. | |||
| 2015-12-05 | Using x in output test-suite Cases.v (cosmetic). | Hugo Herbelin | |
| 2015-12-05 | Ensuring that documentation of mli code works in the presence of utf-8 | Hugo Herbelin | |
| characters. | |||
| 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-05 | Fix CHANGES. | Hugo Herbelin | |
| 2015-12-05 | Getting rid of some quoted tactics in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Specializing the Dyn module to each usecase. | Pierre-Marie Pédrot | |
| Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point. | |||
| 2015-12-04 | Getting rid of the dynamic node of the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-04 | Fix in setoid_rewrite in Type: avoid the generation of a rigid universe | Matthieu Sozeau | |
| on applications of inverse (flip) on a crelation. This was poluting universe constraints of lemmas using generalized rewriting in Type. | |||
| 2015-12-04 | Removing the last use of valueIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Removing dynamic inclusion of constrs in tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-04 | Getting rid of dynamic hacks in Setoid_newring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the globTacticIn primitive. | Pierre-Marie Pédrot | |
| It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee. | |||
| 2015-12-03 | Fixing Tauto compilation for older versions of OCaml. | Pierre-Marie Pédrot | |
| 2015-12-03 | Univs: fix bug #4443. | Matthieu Sozeau | |
| Do not substitute rigid variables during minimization, keeping their equality constraints instead. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |