aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
|
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
| | | | | | 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).
* Adding more sharing in Map.udpate and Map.modify.Gravatar Pierre-Marie Pédrot2015-01-10
|
* Safer version of the implementation of stores.Gravatar Pierre-Marie Pédrot2015-01-06
|
* remove unused iArrayGravatar Enrico Tassi2015-01-06
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
| | | | removing the need of thread creation in the interface.
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
| | | | | I added a emacs_logger. Still need to cleanup std_logger.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
| | | | | | 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.
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
|
* Spawn: fix request of Gc statisticsGravatar Enrico Tassi2014-12-17
|
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
|
* Dyn: add API to check of two Dyn.t are ==Gravatar Enrico Tassi2014-12-17
| | | | | A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API.
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| | | | | Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
* Proper thread-safe implementation for Exninfo.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files.
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-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.
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
| | | | | Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message.
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
|
* Fixing bug #3858 and #3817 in one stroke.Gravatar Pierre-Marie Pédrot2014-12-14
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Better commentGravatar Enrico Tassi2014-12-01
|
* Future: API for blocking futuresGravatar Enrico Tassi2014-11-28
|
* better to always print the thread idGravatar Enrico Tassi2014-11-27
|
* async_queries_* merged with async_proofs_*Gravatar Enrico Tassi2014-11-27
|
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* Making map_union a standard function of the ML library.Gravatar Hugo Herbelin2014-11-19
|
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Removing deprecated code handling color in Pp.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Adding a terminal library.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Move conjugate_verb_to_be next to cString.plural.Gravatar Hugo Herbelin2014-11-13
|
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
|
* Adding a dynamic tag type in Pp.Gravatar Pierre-Marie Pédrot2014-11-10
|
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
| | | | | | printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
* lib/richPp: Fix a bug related to the compatibility with ocaml 3.12Gravatar Yann Régis-Gianas2014-11-05
| | | | | | | - The previous version of this module was using a feature of the Format module of ocaml 4.01. - Add comments.
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/richPp: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
| | | | | A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it.
* lib/Xml_parser.parse: Publish and document new interface.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_printer.pcdata_to_string: Publish.Gravatar Regis-Gianas2014-11-04
|
* printing/RichPrinter: New API for rich pretty-printing.Gravatar Regis-Gianas2014-11-04
| | | | | printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping.
* lib/Pp.rewrite: New.Gravatar Regis-Gianas2014-11-04
| | | | | Allow strings of a pretty-print to be rewritten just before the actual output.
* lib/Xml_printer: Handle non-breakable spaces.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_parser.parse: Make canonicalization optional. (By default, it is ↵Gravatar Regis-Gianas2014-11-04
| | | | applied, to preserve previous behaviors.
* lib/Xml_parser: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* lib/Xml_parser: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Xml_lexer: Handle non-breakable spaces.Gravatar Regis-Gianas2014-11-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 08:20:52 +0000