| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-11-05 | lib/richPp: Fix a bug related to the compatibility with ocaml 3.12 | Yann Régis-Gianas | |
| - The previous version of this module was using a feature of the Format module of ocaml 4.01. - Add comments. | |||
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/richPp: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/Pp.tag: New. | Regis-Gianas | |
| A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | lib/Xml_parser.parse: Publish and document new interface. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_printer.pcdata_to_string: Publish. | Regis-Gianas | |
| 2014-11-04 | printing/RichPrinter: New API for rich pretty-printing. | Regis-Gianas | |
| printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping. | |||
| 2014-11-04 | lib/Pp.rewrite: New. | Regis-Gianas | |
| Allow strings of a pretty-print to be rewritten just before the actual output. | |||
| 2014-11-04 | lib/Xml_printer: Handle non-breakable spaces. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_parser.parse: Make canonicalization optional. (By default, it is ↵ | Regis-Gianas | |
| applied, to preserve previous behaviors. | |||
| 2014-11-04 | lib/Xml_parser: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_parser: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Xml_lexer: Handle non-breakable spaces. | Regis-Gianas | |
| 2014-11-04 | RichPp: New module. | Regis-Gianas | |
| It is responsible for turning a tagged pretty-printing into a semi-structured document. clib.mllib: Include RichPp as well as Xml_*. The migration of Xml_* from lib to clib is needed by RichPp depends on these modules. | |||
| 2014-11-04 | Xml_datatype.gxml: New type for semi-structured documents. | Regis-Gianas | |
| Xml_parser, Xml_printer: Use it. | |||
| 2014-11-04 | lib/Pp: Publish combinators for tags opening and closing. | Regis-Gianas | |
| 2014-11-04 | lib/Pp.ppcmd_token: | Regis-Gianas | |
| Extend this type with Ppcmd_open_tag and Ppcmd_close_tag. lib/Pp.ppcmd_pp_dirs: Handle these tags with a straightforward translation to corresponding Format commands. | |||
| 2014-11-04 | lib/Pp: Cosmetics. | Regis-Gianas | |
| 2014-11-01 | Add an [Info Level] option to print info traces automatically. | Arnaud Spiwack | |
| [Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls. | |||
| 2014-10-31 | Feedback message: hold extra info to help routing | Enrico Tassi | |
| PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |