| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-21 | Future: human readable name for delegated (Close #4065) | Enrico Tassi | |
| 2015-02-16 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise. | |||
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding a statistic function on hashconsing tables. | Pierre-Marie Pédrot | |
| 2015-02-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-07 | Fixing bug #4009. | Pierre-Marie Pédrot | |
| We only allow color output under Unix OSes. | |||
| 2015-02-06 | More efficient Richpp. | Pierre-Marie Pédrot | |
| We build the rich XML at once without generating the printed string. | |||
| 2015-02-05 | Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968) | Enrico Tassi | |
| Strings are at most 16M on 32 bit OCaml, and the system state may be bigger. In this case we write to tmp file and Marshal.from_channel. We can't directly use the channel interface because of badly designed non blocking API (available only on fds and not channels). | |||
| 2015-02-04 | More efficient implementation of Richpp. | Pierre-Marie Pédrot | |
| Instead of constructing the XML string and parsing it afterwards, we build it by hijacking the formatting output. | |||
| 2015-02-04 | CThread: workaround for threads lockup on windwos made more aggressive | Enrico Tassi | |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-01-25 | Equipping extended maps with fold operator defined for any monad. | Pierre-Marie Pédrot | |
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2015-01-12 | Fix a few typos. | Maxime Dénès | |
| 2015-01-11 | Extraction: no more ascii blob in type variables (fix #3227) | Pierre Letouzey | |
| Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral). | |||
| 2015-01-10 | Adding more sharing in Map.udpate and Map.modify. | Pierre-Marie Pédrot | |
| 2015-01-06 | Safer version of the implementation of stores. | Pierre-Marie Pédrot | |
| 2015-01-06 | remove unused iArray | Enrico Tassi | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2014-12-25 | Inlining Spawn.kill_if in the one place were it was actually used, thus | Pierre-Marie Pédrot | |
| removing the need of thread creation in the interface. | |||
| 2014-12-18 | Fixed bad newlines in output for std output and emacs. | Pierre Courtieu | |
| I added a emacs_logger. Still need to cleanup std_logger. | |||
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot | |
| 2014-12-17 | Future: blocking by default | Enrico Tassi | |
| This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script. | |||
| 2014-12-17 | STM: rename and simplify flags | Enrico Tassi | |
| 2014-12-17 | Spawn: fix request of Gc statistics | Enrico Tassi | |
| 2014-12-17 | CThread: use a different type for thread friendly in_channels | Enrico Tassi | |
| 2014-12-17 | Dyn: add API to check of two Dyn.t are == | Enrico Tassi | |
| A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API. | |||
| 2014-12-16 | msg_info now puts infomsg tag in emacs mode. | Pierre Courtieu | |
| Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal. | |||
| 2014-12-16 | Proper thread-safe implementation for Exninfo. | Pierre-Marie Pédrot | |
| This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files. | |||
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-12-15 | Changed bullet informations to warning for better display in PG. | Pierre Courtieu | |
| Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message. | |||
| 2014-12-14 | Util.un_op -> Option.default | Pierre Boutillier | |
| 2014-12-14 | Fixing bug #3858 and #3817 in one stroke. | Pierre-Marie Pédrot | |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-01 | Better comment | Enrico Tassi | |
| 2014-11-28 | Future: API for blocking futures | Enrico Tassi | |
| 2014-11-27 | better to always print the thread id | Enrico Tassi | |
| 2014-11-27 | async_queries_* merged with async_proofs_* | Enrico Tassi | |
| 2014-11-27 | Feedback: API cleaned up, documented and made user extensible | Enrico Tassi | |
| 2014-11-19 | Making map_union a standard function of the ML library. | Hugo Herbelin | |
| 2014-11-15 | Reworking the -color flag of coqtop. | Pierre-Marie Pédrot | |
| 2014-11-15 | Removing deprecated code handling color in Pp. | Pierre-Marie Pédrot | |
| 2014-11-15 | Adding a terminal library. | Pierre-Marie Pédrot | |
| 2014-11-13 | Move conjugate_verb_to_be next to cString.plural. | Hugo Herbelin | |
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-11-10 | Adding a dynamic tag type in Pp. | Pierre-Marie Pédrot | |
| 2014-11-05 | lib/RichPp: Rename into Richpp. | Yann Régis-Gianas | |
| printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |