| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-02-12 | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | |
| The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes. | |||
| 2014-02-11 | Made Pre_env.lazy_val opaque. | Pierre-Marie Pédrot | |
| 2014-02-10 | Timeout and Set Default Timeout fixed (closes: #3229) | Enrico Tassi | |
| 2014-02-10 | STM: fix valid_id coming from Qed errors | Enrico Tassi | |
| 2014-02-10 | STM: when a worker is canceled mark the proof as broken | Enrico Tassi | |
| 2014-02-10 | STM: be conservative w.r.t. proofs containing global side effects | Enrico Tassi | |
| 2014-02-10 | fake_ide: ported to spawn | Enrico Tassi | |
| 2014-02-10 | Tentative fixup for the previous commit. It seems I have broken something | Pierre-Marie Pédrot | |
| nasty relating memory management triggering random segfaults. But this seemed really unlikely... | |||
| 2014-02-09 | Small optimizations in Closure: | Pierre-Marie Pédrot | |
| 1. Only apply last Zupdates 2. Better smartmap with state. | |||
| 2014-02-08 | Less dependencies in Omega. | Pierre-Marie Pédrot | |
| 2014-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ↵ | Pierre Letouzey | |
| domains + Some extra results about NoDup, Fin.t, ... | |||
| 2014-02-05 | Tactic extensions do not need to be classified by the STM, as | Pierre-Marie Pédrot | |
| they never produce a VernacExtend entry. | |||
| 2014-02-04 | The constructor tactic now returns several successes. | Pierre-Marie Pédrot | |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot | |
| 2014-02-03 | Allocation-friendly mapping functions in Nametab. | Pierre-Marie Pédrot | |
| 2014-02-03 | Allocation friendly map-handling functions in Dag. | Pierre-Marie Pédrot | |
| 2014-02-02 | Fixing backtrace reporting. | Pierre-Marie Pédrot | |
| 2014-02-02 | Fixing bug #3226. | Pierre-Marie Pédrot | |
| 2014-02-02 | Removing the [Require "file"] syntax. | Pierre-Marie Pédrot | |
| 2014-01-31 | In Ltac's exact tactic: avoid checking the type of the term twice. | Arnaud Spiwack | |
| Following a remark by Jason Gross and Daniel Grayson. | |||
| 2014-01-31 | Typos in comment. | Arnaud Spiwack | |
| 2014-01-30 | Coqmktop without Sys.command, changes in ./configure -*byteflags options | Pierre Letouzey | |
| NB: Please re-run ./configure after pulling this commit For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore, but rather CUnix.sys_command, which is based on Unix.create_process. This way, we do not need to bother with the underlying shell (/bin/sh or cmd.exe) and the way arguments are to be quoted :-). Btw, many cleanups of coqmktop. Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option" that collect as a string several sub-options to be given by coqmktop to ocamlc. For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to parse all these sub-options. To ease that, I've made the following changes to the ./configure options: * The -coqrunbyteflags and its blank-separated argument isn't accepted anymore, and is replaced by a new option -vmbyteflags which expects a comma-separated argument. For instance: ./configure -vmbyteflags "-dllib,-lcoqrun" Btw, on this example, the double-quotes aren't mandatory anymore :-) * The -coqtoolsbyteflags isn't accepted anymore. To the best of my knowledge, nobody ever used it directly (it was internally triggered as a byproduct of the -custom option). The only interest I can think of for this option was to cancel the default use of ocamlc custom-linking on Win32 and MacOS. For that, ./configure now provides a -no-custom option. | |||
| 2014-01-30 | Relaunch all Unix.waitpid when they ended with EINTR | Pierre Letouzey | |
| Moreover, cleanup of System.connect (used by the "external" tactic). | |||
| 2014-01-30 | CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned | Pierre Letouzey | |
| 2014-01-30 | Mltop: explicitly qualify calls to CUnix | Pierre Letouzey | |
| 2014-01-30 | CString: avoid redefining is_sub | Pierre Letouzey | |
| 2014-01-30 | Remove useless Xml_utils | Pierre Letouzey | |
| 2014-01-30 | Get rid of two utility files, obsolete now that configure is a .ml | Pierre Letouzey | |
| 2014-01-30 | clib.mllib: remove duplicated Flags entry | Pierre Letouzey | |
| 2014-01-30 | G_xml: remove some duplication in error fonctions | Pierre Letouzey | |
| 2014-01-30 | G_xml: protect against some possible Not_found | Pierre Letouzey | |
| 2014-01-30 | Load implemented in CoqIDE/STM (closes: #3223) | Enrico Tassi | |
| 2014-01-30 | STM + CoqIDE: stop_worker message and UI | Enrico Tassi | |
| 2014-01-30 | Work around for bug in threads + blocking io streamlined | Enrico Tassi | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |