coq - The formal proof system

Age	Commit message (Expand)	Author
2014-11-05	lib/richPp: Fix a bug related to the compatibility with ocaml 3.12	Yann Régis-Gianas
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
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
2014-11-04	lib/Pp.rewrite: New.	Regis-Gianas
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 appl...	Regis-Gianas
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
2014-11-04	Xml_datatype.gxml: New type for semi-structured documents.	Regis-Gianas
2014-11-04	lib/Pp: Publish combinators for tags opening and closing.	Regis-Gianas
2014-11-04	lib/Pp.ppcmd_token:	Regis-Gianas
2014-11-04	lib/Pp: Cosmetics.	Regis-Gianas
2014-11-01	Add an [Info Level] option to print info traces automatically.	Arnaud Spiwack
2014-10-31	Feedback message: hold extra info to help routing	Enrico Tassi
2014-10-31	STM: new worker for queries	Enrico Tassi
2014-10-25	Changed implementation of lib/heap.ml to use Braun trees	Jean-Christophe Filliatre
2014-10-24	-help failing (fix 3762)	Enrico Tassi
2014-10-23	Monad: change the error managing of two-list combinators.	Arnaud Spiwack
2014-10-22	Goal printing made uniform: always done in STM (close 3585)	Enrico Tassi
2014-10-22	An additional [List.iter] monadic combinator.	Arnaud Spiwack
2014-10-22	Add more primitives to the [Monad.Make] arguments.	Arnaud Spiwack
2014-10-22	Proofview: move [list_goto] to the [CList] module.	Arnaud Spiwack
2014-10-22	Add a two-list monadic fold_left iterator.	Arnaud Spiwack
2014-10-22	Small optimisation in the monadic list combinators.	Arnaud Spiwack
2014-10-22	Factor module signatures.	Arnaud Spiwack
2014-10-13	When loading libraries, feed back dependencies.	Carst Tankink
2014-10-13	STM: primitives to snapshot a .vi while in interactive mode	Enrico Tassi
2014-10-13	library/opaqueTables: enable their use in interactive mode	Enrico Tassi
2014-10-09	Fixup leading ./ path cleaning	Pierre Boutillier
2014-10-07	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin
2014-10-05	A few improvements on pattern-matching compilation.	Hugo Herbelin
2014-10-01	STM: report the (structured) goals as XML	Carst Tankink
2014-09-25	Remove some 'deprecated' warnings.	Xavier Clerc
2014-09-18	Fix debug printing with primitive projections.	Matthieu Sozeau
2014-09-16	Undo prints only if coqtop \|\| emacs	Enrico Tassi
2014-09-09	Undo: if the ui is coqtop (command line) then Undo is not part of the doc.	Enrico Tassi
2014-09-09	toploop plugins taken into account when printing --help (close: 3535)	Enrico Tassi
2014-09-08	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot
2014-09-05	Adding a Ftactic module for potentially focussing tactics.	Pierre-Marie Pédrot
2014-09-02	coqworkmgr	Enrico Tassi
2014-08-29	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot
2014-08-29	Simplification of Genarg unpackers.	Pierre-Marie Pédrot
2014-08-28	Fixing bug #3541.	Pierre-Marie Pédrot