coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-05-13	Dyn: simplify API introducing an Easy submodule	Enrico Tassi
	Now the casual Dyn user does not need to be a GADT guru
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

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

2016-01-17	Adding a structure indexed by tags.	Pierre-Marie Pédrot

2015-12-05	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot

2015-12-04	Specializing the Dyn module to each usecase.	Pierre-Marie Pédrot
	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.
2015-03-16	Adding a primitive to dump the current association table of dynamic types.	Pierre-Marie Pédrot

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

2014-12-17	Dyn: add API to check of two Dyn.t are ==	Enrico Tassi
	A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API.
2013-11-22	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot
	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.
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
	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
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
	- 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
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
	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
2004-07-16	Nouvelle en-tête	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15	entetes	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-17	ajout dyn; divers fonctions util	filliatr
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8 85f007b7-540e-0410-9357-904b9bb8a0f7