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-12-05	Rename update to set, fixes #6196	Paul Steckler

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-08-22	Fast path for set operations.	Pierre-Marie Pédrot
	We consider an approximation of the size of sets before choosing the most appropriate algorithm. This drastically affects some universe-polymorphic code which was doing a lot of set operations on disimilar sizes.
2016-02-03	Adding a "get" primitive to map signature.	Pierre-Marie Pédrot
	It is similar to find but raises an assertion failure instead of a Not_found when the element is not encountered. Using it will give stronger invariants.
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

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

2016-01-06	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond
	Conflicts: lib/cSig.mli
2016-01-06	Protect code against changes in Map interface.	Maxime Dénès
	The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps.
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

2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
	It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
2014-03-05	Fixing compilation on OCaml 4.01.	Pierre-Marie Pédrot

2014-01-29	Adding a smartmap[i] operator to maps.	Pierre-Marie Pédrot

2013-11-24	Adding fold_left / fold_right function to maps.	Pierre-Marie Pédrot

2013-11-13	Adding an unsafe mapping function to maps.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17085 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04	Added an update function in CMap. It has the same signature as Map.add, but	ppedrot
	expects the given key to be present, and thus is faster. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17051 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06	Added a [modify] function to maps.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25	Removing association lists in Reductionops. Btw, defining the dual of the	ppedrot
	domain operation on maps. The efficiency should just be improved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16737 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
	The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7