| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update headers following #6543. |  Théo Zimmermann | 2018-02-27 |
| | | |||
| * | [flags] [stm] Reorganize flags. |  Emilio Jesus Gallego Arias | 2017-12-11 |
| | | | | | | | | | We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag. | ||
| * | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | 2017-11-24 |
| | | | | | | We also remove some internal implementation details from the mli file, there due historical reasons. | ||
| * | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. |  Maxime Dénès | 2017-07-21 |
| | | |||
| * | Bump year in headers. |  Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| | | |||
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| | | |||
| * | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
| | | | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads. | ||
| * | STM: code restructured to reuse task queue for tactics |  Enrico Tassi | 2014-08-05 |
| | | |||
| * | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi | 2014-07-10 |
| | | | | | | Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay. | ||
| * | Less ocaml warnings. |  Hugo Herbelin | 2014-06-21 |
| | | |||
| * | Timeout implementation for Windows based on threads. | Pierre-Marie Pédrot | 2014-06-08 |
| | | |||
| * | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot | 2014-06-07 |
| | | |||
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |