| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Rename Ephemeron -> CEphemeron. |  Maxime Dénès | 2016-03-04 |
| | | | | | Fixes compilation of Coq with OCaml 4.03 beta 1. | ||
| * | Fix a typo in dev/doc/changes.txt |  Jason Gross | 2016-03-04 |
| | | | | CQQ -> COQ | ||
| * | Adding a test for the behaviour of open_constr described in #3777. |  Pierre-Marie Pédrot | 2016-03-03 |
| | | |||
| * | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. | Pierre-Marie Pédrot | 2016-03-03 |
| | | | | | | | | Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. | ||
| * | Fixing bug #4596: [rewrite] broke in the past few weeks. | Pierre-Marie Pédrot | 2016-02-28 |
| | | | | | | | Checking that a term was indeed a relation was made too early, as the decomposition function recognized relations of the form "f (g .. (h x y)) with f, g unary and only h binary. We postpone this check to the very end. | ||
| * | Document Hint Mode, cleanup Hint doc. |  Matthieu Sozeau | 2016-02-24 |
| | | |||
| * | Document differences of Hint Resolve and Hint Extern | Matthieu Sozeau | 2016-02-23 |
| | | |||
| * | Fix part of bug #4533: respect declared global transparency of | Matthieu Sozeau | 2016-02-23 |
| | | | | | projections in unification.ml | ||
| * | Fix bug #4544: Backtrack on using full betaiota reduction during keyed ↵ | Matthieu Sozeau | 2016-02-23 |
| | | | | | unification. | ||
| * | Fixing bug #4540: CoqIDE bottom progress bar does not update. | Pierre-Marie Pédrot | 2016-02-20 |
| | | |||
| * | Fix regression from 8.4 in reflexivity/... |  Matthieu Sozeau | 2016-02-19 |
| | | | | | | reflexivity/symmetry/transitivity only need RelationClasses to be loaded. | ||
| * | Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance. | Pierre-Marie Pédrot | 2016-02-19 |
| | | |||
| * | Fixing bug #4582: cannot override notation [ x ]. | Pierre-Marie Pédrot | 2016-02-19 |
| | | |||
| * | STM: Print/Extraction have to be skipped if -quick |  Enrico Tassi | 2016-02-19 |
| | | | | | | | | | | | | | Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull. | ||
| * | 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 | 2016-02-19 |
| | | | | | | | | | | | | "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. | ||
| * | Fixing the Proofview.Goal.goal function. | Pierre-Marie Pédrot | 2016-02-17 |
| | | | | | | The environment put in the goals was not the right one and could lead to various leaks. | ||
| * | Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). | Pierre-Marie Pédrot | 2016-02-17 |
| | | | | | | 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. | ||
| * | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot | 2016-02-13 |
| | | | | | | | | | 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. | ||
| * | STM: always stock in vio files the first node (state) of a proof | Enrico Tassi | 2016-02-10 |
| | | | | | | | | | 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 | ||
| * | 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 | 2016-02-10 |
| | | | | | This fixes micromega in certain environments. | ||
| * | Improving error message with missing patterns in the presence of |  Hugo Herbelin | 2016-02-08 |
| | | | | | multiple patterns. | ||
| * | Optimizing the universes_of_constr_function. | Pierre-Marie Pédrot | 2016-02-03 |
| | | | | | | Instead of relying on a costly set union, we take advantage of the fact that instances are small compared to the set of universes. | ||
| * | 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 | 2016-02-03 |
| | | | | | This patch was proposed by JH in bug report #4547. | ||
| * | Fix bug #4537: Coq 8.5 is slower in typeclass resolution. | Pierre-Marie Pédrot | 2016-01-27 |
| | | | | | | | | 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. | ||
| * | Fixing bde12b70 about reporting ill-formed constructor. | Hugo Herbelin | 2016-01-26 |
| | | | | | | | | | 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. | ||
| * | 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 | 2016-01-24 |
| | | | | | | | 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. | ||
| * | Fixing bug #4511: evar tactic can create non-typed evars. | Pierre-Marie Pédrot | 2016-01-24 |
| | | |||
| * | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau | 2016-01-23 |
| | | | | | variables and definitions in sections is unsupported. | ||
| * | 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 | 2016-01-23 |
| | | | | | Fixpoint/Definition. | ||
| * | Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form | Matthieu Sozeau | 2016-01-23 |
| | | | | | | (let x := t in u) a that should be reduced. Maybe a different decomposition/reduction primitive should be used instead. | ||
| * | Restore warnings produced by the interpretation of the command line | Hugo Herbelin | 2016-01-22 |
| | | | | | | | | (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb. | ||
| * | Compile OS X binaries without native_compute support. | Maxime Dénès | 2016-01-21 |
| | | |||
| * | 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 | 2016-01-20 |
| | | | | | | | This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. | ||
| * | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin | 2016-01-20 |
| | | | | | Following a discussion on coq-club on Jan 13, 2016. | ||
| * | Fixing Not_found on unknown bullet behavior. | Hugo Herbelin | 2016-01-20 |
| | | |||
| * | Fix bug #4420: check_types was losing universe constraints. | Matthieu Sozeau | 2016-01-19 |
| | | |||
| * | Thanks Hugo, but let's remain factual. | Maxime Dénès | 2016-01-15 |
| | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |