| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the last use of tacticIn in setoid_ring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the use of tacticIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-02 | Adding a target report to test-suite's Makefile to get a short summary. | Hugo Herbelin | |
| 2015-12-02 | Slight simplification of code for pat/constr. | Hugo Herbelin | |
| 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 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
| 2015-12-02 | Update history of revisions. | Hugo Herbelin | |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-12-02 | Univs/Program: update the universe context with global universe | Matthieu Sozeau | |
| constraints at the time of Next Obligation/Solve Obligations so that interleaving definitions and obligation solving commands works properly. | |||
| 2015-12-02 | Fix bug #4444: Next Obligation performed after a Section opening was | Matthieu Sozeau | |
| using the wrong context. This is very bad style but currently unavoidable, at least we don't throw an anomaly anymore. | |||
| 2015-12-02 | Add an option to deactivate compatibility printing of primitive | Matthieu Sozeau | |
| projections (off by default). | |||
| 2015-12-02 | Fix a bug in externalisation which prevented printing of projections | Matthieu Sozeau | |
| using dot notation. | |||
| 2015-12-02 | Removing dead code in Obligations. | Pierre-Marie Pédrot | |
| 2015-12-01 | New algorithm for universe cycle detections. | Jacques-Henri Jourdan | |
| 2015-12-01 | Remove unneeded fixpoint in normalize_context_set. Note that it is no | Matthieu Sozeau | |
| longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l). | |||
| 2015-12-01 | vio: fix argument parsing (progress on #4442) | Enrico Tassi | |
| 2015-11-30 | Simplify coqdep lexer by removing global references. | Guillaume Melquiond | |
| 2015-11-30 | Test for bug #4149. | Pierre-Marie Pédrot | |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-28 | Test-suite files for closed bugs | Matthieu Sozeau | |
| 2015-11-28 | Closed bugs. | Matthieu Sozeau | |
| 2015-11-28 | Univs: correctly register universe binders for lemmas. | Matthieu Sozeau | |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | |
| Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |