coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.	Maxime Dénès	2017-11-03
\|\
* \|	Naming the type of Dyn.Map for future reuse.	Hugo Herbelin	2017-11-02
\| \|
\| *	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
\|/ \| \| \|	4.02.3 has been the minimal OCaml version for a while now.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	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
\| \|
* \|	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.
*	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.
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 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
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
\| \| \| \| \| \|	Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 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
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 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
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 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