coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-12-23	[lib] Split auxiliary libraries into Coq-specific and general.	Emilio Jesus Gallego Arias
	Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-03-10	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-07-24	Revert "Adding a "is_val" primitive to IStream."	Pierre-Marie Pédrot
	This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92.
2014-07-22	Adding a "is_val" primitive to IStream.	Pierre-Marie Pédrot

2014-07-03	Adding a coiterator to IStream.	Pierre-Marie Pédrot

2014-03-05	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey
	The removed code isn't used locally and isn't exported in the signature
2014-02-24	IStream: more efficient implementation of concat_map.	Arnaud Spiwack

2014-02-24	IStream: a concat_map primitive.	Arnaud Spiwack

2014-02-24	IStream: change type of thunk, spare allocations.	Arnaud Spiwack
	Two changes: - 'a Lazy.t becomes unit -> 'a - 'a t becomes 'a u (the view type) This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.
2014-02-24	IStream: remove a useless Obj.magic.	Arnaud Spiwack
	Lazy.lazy_from_val does almost the same thing as this Obj.magic. It makes some extra dynamic check, but it's frankly unlikely that it could be observed.
2014-02-24	A view type for IStream.	Arnaud Spiwack
	View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
2013-11-06	better IStream.concat	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17064 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08	Small fix in IStream interface.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-29	More clever implemenation for IStream.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16538 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-28	Adding a persistent stream data structure.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7