| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-02-19 | CoqIDE: STOP button also stops workers (fix #4542) | Enrico Tassi | |
| 2016-02-19 | STM: classify some variants of Instance as regular `Fork nodes. | Enrico Tassi | |
| "Instance name : Type." is like "Lemma name : Type", i.e. it starts a proof. Unfortunately sometimes it does not, so we say VtUnknown. Still, if there is an open proof, we classify it as a regular Lemma, i.e. the opacity depends only on the terminator. This makes CoqIDE and PIDE based UI way more responsive when processing files containing Instance that are proved by tactics, since they are now correctly delegated to workers. Bug reported privately by Alec Faithfull. | |||
| 2016-02-17 | Fixing the Proofview.Goal.goal function. | Pierre-Marie Pédrot | |
| The environment put in the goals was not the right one and could lead to various leaks. | |||
| 2016-02-17 | Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). | Pierre-Marie Pédrot | |
| The setoid_rewrite tactic was not checking that the relation it was looking for was indeed a relation, i.e. that its type was an arity. | |||
| 2016-02-13 | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot | |
| The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. | |||
| 2016-02-10 | STM: always stock in vio files the first node (state) of a proof | Enrico Tassi | |
| It used not to be the case when the proof contains Sideff, since the code was picking the last known state and not necessarily the first one. Because of side effects the last known state could be the one corresponding to the side effect (that was executed to, say, change the parser). This is also related to bug #4530 | |||
| 2016-02-10 | STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 | Enrico Tassi | |
| 2016-02-10 | Don't fail fatally if PATH is not set. | Emilio Jesus Gallego Arias | |
| This fixes micromega in certain environments. | |||
| 2016-02-08 | Improving error message with missing patterns in the presence of | Hugo Herbelin | |
| multiple patterns. | |||
| 2016-02-03 | Optimizing the universes_of_constr_function. | Pierre-Marie Pédrot | |
| Instead of relying on a costly set union, we take advantage of the fact that instances are small compared to the set of universes. | |||
| 2016-02-03 | Optimizing the computation of frozen evars. | Pierre-Marie Pédrot | |
| 2016-02-03 | Opacifying the type of evar naming structure in Evd. | Pierre-Marie Pédrot | |
| 2016-02-03 | More compact representation for evar resolvability flag. | Pierre-Marie Pédrot | |
| This patch was proposed by JH in bug report #4547. | |||
| 2016-01-27 | Fix bug #4537: Coq 8.5 is slower in typeclass resolution. | Pierre-Marie Pédrot | |
| The performance enhancement introduced by a895b2c0 for non-polymorphic hints was actually causing a huge regression in the polymorphic case (and was marked as such). We fix this by only substituting the metas from the evarmap instead of the whole evarmap. | |||
| 2016-01-26 | Fixing bde12b70 about reporting ill-formed constructor. | Hugo Herbelin | |
| For instance, in Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0. the computation of the number of arguments to I was made wrong in bde12b70. | |||
| 2016-01-24 | Tentative fix for bug #4522: Incorrect "Warning..." on windows. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #4373: coqdep does not know about .vio files. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #3826: "Incompatible module types" is uninformative. | Pierre-Marie Pédrot | |
| 2016-01-24 | Adding a test for bug #4378. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #4495: Failed assertion in metasyntax.ml. | Pierre-Marie Pédrot | |
| We simply handle the "break" in error messages. Not sure it is the proper bugfix though, we may want to be able to add breaks in such recursive notations. | |||
| 2016-01-24 | Fixing bug #4511: evar tactic can create non-typed evars. | Pierre-Marie Pédrot | |
| 2016-01-23 | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau | |
| variables and definitions in sections is unsupported. | |||
| 2016-01-23 | Fix bug #4519: oops, global shadowed local universe level bindings. | Matthieu Sozeau | |
| 2016-01-23 | Implement support for universe binder lists in Instance and Program ↵ | Matthieu Sozeau | |
| Fixpoint/Definition. | |||
| 2016-01-23 | Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form | Matthieu Sozeau | |
| (let x := t in u) a that should be reduced. Maybe a different decomposition/reduction primitive should be used instead. | |||
| 2016-01-22 | Restore warnings produced by the interpretation of the command line | Hugo Herbelin | |
| (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb. | |||
| 2016-01-21 | Compile OS X binaries without native_compute support. | Maxime Dénès | |
| 2016-01-20 | Update cic.mli MD5 after header update. | Maxime Dénès | |
| 2016-01-20 | Update version number in configure. | Maxime Dénès | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-20 | Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. | Maxime Dénès | |
| 2016-01-20 | Documenting Set Bullet Behavior. | Hugo Herbelin | |
| This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. | |||
| 2016-01-20 | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin | |
| Following a discussion on coq-club on Jan 13, 2016. | |||
| 2016-01-20 | Fixing Not_found on unknown bullet behavior. | Hugo Herbelin | |
| 2016-01-19 | Fix bug #4420: check_types was losing universe constraints. | Matthieu Sozeau | |
| 2016-01-15 | Thanks Hugo, but let's remain factual. | Maxime Dénès | |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès | |
| 2016-01-15 | Minor edits in output of coqdep --help. | Maxime Dénès | |
| 2016-01-15 | Fix #4408. | Pierre Courtieu | |
| Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others. | |||
| 2016-01-15 | Partially fixing #4408: coqdep --help is up to date. | Pierre Courtieu | |
| 2016-01-13 | MMaps: remove it from final 8.5 release, since this new library isn't mature ↵ | Pierre Letouzey | |
| enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now. | |||
| 2016-01-13 | Fixing success of test for #3848 after move to directory "closed". | Hugo Herbelin | |
| 2016-01-13 | Fixing #4467 (continued). | Hugo Herbelin | |
| Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v). | |||
| 2016-01-12 | Fixing #4467 (missing shadowing of variables in cases pattern). | Hugo Herbelin | |
| This fixes a TODO in map_constr_expr_with_binders, a bug in is_constructor, as well as a bug and TODOS in ids_of_cases_indtype. | |||
| 2016-01-12 | Fixing #4256 and #4484 (changes in evar-evar resolution made that new | Hugo Herbelin | |
| evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details. | |||
| 2016-01-12 | Reporting about the new tactical unshelve. | Hugo Herbelin | |
| 2016-01-12 | Extend last commit: keyed unification uses full conversions on the applied ↵ | Matthieu Sozeau | |
| constant and arguments _separately_. | |||
| 2016-01-12 | Extend Keyed Unification tests with the one from R. Krebbers. | Matthieu Sozeau | |
| 2016-01-12 | Fix essential bug in new Keyed Unification mode reported by R. Krebbers. | Matthieu Sozeau | |
| [rewrite] was calling find_suterm using the wrong unification flags, not allowing full delta in unification of terms with the right keys as desired. | |||
| 2016-01-12 | Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |