| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-01-30 | STM: worker sends back to master the last valid state | Enrico Tassi | |
| So that the master process does not require to compute it. Still not all valid states are sent back. | |||
| 2014-01-30 | STM: tell the user if the master is recomputing states validated by workers | Enrico Tassi | |
| When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly. | |||
| 2014-01-30 | Fixing backtrace handling here and there. | Pierre-Marie Pédrot | |
| 2014-01-29 | Using Map.smartmap whenever deemed useful. | Pierre-Marie Pédrot | |
| 2014-01-29 | Adding a smartmap[i] operator to maps. | Pierre-Marie Pédrot | |
| 2014-01-28 | Fixing dependent inversion. Some exceptions were not caught by the tactic | Pierre-Marie Pédrot | |
| monad. | |||
| 2014-01-27 | Abstracting away coercion indexes in Classops. | Pierre-Marie Pédrot | |
| 2014-01-26 | Coercions: avoid imperative data structure | Enrico Tassi | |
| 2014-01-26 | -schedule-vi-checking ported to spawn | Enrico Tassi | |
| 2014-01-26 | CoqIDE: command line for extra coqtop "flags" | Enrico Tassi | |
| Like the socket for the OCaml debugger | |||
| 2014-01-26 | break > 80 cols line | Enrico Tassi | |
| 2014-01-26 | STM: ported to spawn | Enrico Tassi | |
| 2014-01-26 | CoqIDE: ported to spawn | Enrico Tassi | |
| 2014-01-26 | Spawn: managed processes | Enrico Tassi | |
| The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively. | |||
| 2014-01-26 | configure.ml fixed wrt Win32 + byte-only + coqide | Enrico Tassi | |
| 2014-01-25 | Adding a test for bug #3023. | Pierre-Marie Pédrot | |
| 2014-01-25 | More in CHANGES. | Pierre-Marie Pédrot | |
| 2014-01-24 | [Coercion]s use [Sortclass], not [Prop] (in docs) | Jason Gross | |
| Reported By: J. Ian Johnson | |||
| 2014-01-24 | The configure script now outputs the parameters it was fed with in | Pierre-Marie Pédrot | |
| config/coq_config.ml | |||
| 2014-01-20 | bug correction in proving principles of function | jforest | |
| 2014-01-19 | Using full paths in coqdep -dumpgraph. | Pierre-Marie Pédrot | |
| 2014-01-19 | Fixing coqdep graph printing. The transitive reduction algorithm was bugged. | Pierre-Marie Pédrot | |
| 2014-01-19 | Adding a default object to generic argument registering mechanism. | Pierre-Marie Pédrot | |
| 2014-01-19 | Fixing an interpretation bug with tactics in notations. For some obscure | Pierre-Marie Pédrot | |
| reason, Ltac interpretation does not allow tactics of the following shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics and build the resulting hole tactic from scratch. | |||
| 2014-01-19 | Fixing checker compilation, which was broken by the following commit: | Pierre-Marie Pédrot | |
| 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369 | |||
| 2014-01-18 | Relaxing the sort elimination check to allow for let-bindings in arities. | Maxime Dénès | |
| I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed. | |||
| 2014-01-18 | Makefiles use $(foo), not $foo, for variables | Jason Gross | |
| Also, we need :=, so that it's evaluated immediately, rather than becoming a self-recursive variable. This fixes the "Undefined variable 'C'" error that make keeps spewing. | |||
| 2014-01-18 | Fixup make clean and .merlin | Pierre Boutillier | |
| 2014-01-17 | Follow-up of bugfix for #3204: local definitions were not handled properly. | Pierre-Marie Pédrot | |
| 2014-01-17 | Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵ | Pierre-Marie Pédrot | |
| hypothesis. | |||
| 2014-01-17 | Update .mailmap with recent contributors. | Arnaud Spiwack | |
| I should have updated everyone who committed since the migration to git (giving me a canonical email). I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed. | |||
| 2014-01-16 | Fixing bugs #1039: Hypotheses don't respect Barendregt convention | Pierre-Marie Pédrot | |
| and #3204: Failure of hygiene condition. It was sufficient to tweak a flag in the constr externalization... | |||
| 2014-01-16 | Implementing transitive reduction in the dependency graph printing | Pierre-Marie Pédrot | |
| mechanism of coqdep. | |||
| 2014-01-15 | Christmas is over... | Maxime Dénès | |
| 2014-01-15 | Test case containing a proof of false due to a DeBruijn off-by-one error in the | Maxime Dénès | |
| code checking allowed sorts for elimination. | |||
| 2014-01-14 | -schedule-vi-checking generates better script | Enrico Tassi | |
| 2014-01-14 | STM: fix -async-proofs lazy | Enrico Tassi | |
| 2014-01-14 | Removing unused tactics in rewrite. | Pierre-Marie Pédrot | |
| 2014-01-13 | Make Require verbose | Pierre Boutillier | |
| 2014-01-13 | rename Paral-ITP demo file | Enrico Tassi | |
| 2014-01-13 | Paral-ITP demo: better comments | Enrico Tassi | |
| 2014-01-13 | STM: fix very simple demo | Enrico Tassi | |
| 2014-01-13 | Declared ML Module are not uncapitalized/capitalized/uncapitalized/... | Pierre Boutillier | |
| The exact filename has to be written. This is coherent with the RefMan. | |||
| 2014-01-13 | Fixing typo in reference manual from previous commit | Hugo Herbelin | |
| 2014-01-13 | Documenting old but useful command "Print Tables". | Hugo Herbelin | |
| Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual. | |||
| 2014-01-11 | 'Pretty' printer for wf_paths | Pierre | |
| 2014-01-10 | Fixing bug #3144. | Pierre-Marie Pédrot | |
| 2014-01-10 | Useless Array.of_list | Pierre-Marie Pédrot | |
| 2014-01-10 | Omega: avoiding distinct proof-terms on repeated identical runs | Pierre Letouzey | |
| Omega now reuse the same inner variable names (Zvar0, Zvar1, ...) at each run. This way, the obtained proof-terms on two identical omega runs should be the same. This wasn't always the case earlier: - the two proofs were almost always convertible, but with distinct variable names. - in very rare situations, the two proofs could even be non-convertible. Indeed, the omega engine use hash-tables which may be sensible to the names in the (in)equality system and hence lead to different solutions. Example of this behavior (with ocaml 4, whose default hash function is different from ocaml 3.12, leading to a different behavior here !) : -------------------------------------------------------------------- Require Import Omega. Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Check (eq_refl : test1 = test2). (* OK *) Check (eq_refl : test1 = test3). (* OK *) Check (eq_refl : test1 = test4). (* KO, test4 is different !! *) -------------------------------------------------------------------- The old behavior could be restored with "Unset Stable Omega". Thanks to Frédéric Loulergue for spotting this sensibility to the underlying ocaml versions... | |||
| 2014-01-10 | Exporting the full pretyper options in Goal.constr_of_raw. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |