coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Dyn: simplify API introducing an Easy submodule	Enrico Tassi	2016-05-13
\| \| \| \|	Now the casual Dyn user does not need to be a GADT guru
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Adding a structure indexed by tags.	Pierre-Marie Pédrot	2016-01-17
\| \|
* \|	Factorizing unsafe code by relying on the new Dyn module.	Pierre-Marie Pédrot	2015-12-05
\| \|
* \|	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05
\| \|
* \|	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot	2015-12-04
\|/ \| \| \| \| \|	Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| \| \| \| \| \|	Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
*	Adding a primitive to dump the current association table of dynamic types.	Pierre-Marie Pédrot	2015-03-16
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Dyn: add API to check of two Dyn.t are ==	Enrico Tassi	2014-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.
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
\| \| \| \| \| \| \| \|	anomaly is raised. As there are very few tags defined in Coq code, this is very unlikely to appear, and can be fixed by tweaking the name of the dynamic argument. This should be more efficient, as we did compare equal strings each time.
*	Removing some lone List.assoc & List.mem in lib.	ppedrot	2013-08-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
\| \| \| \| \| \|	Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
\| \| \| \| \| \| \| \| \| \|	compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Noise for nothing	pboutill	2012-03-02
\| \| \| \| \| \| \| \| \| \| \|	Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de divers fonctions dans lib/	filliatr	1999-09-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@82 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout dyn; divers fonctions util	filliatr	1999-08-17
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8 85f007b7-540e-0410-9357-904b9bb8a0f7