coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Updating headers.	herbelin	2012-08-08
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	unification encore...	barras	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	Nouvelle en-tête	herbelin	2004-07-16
*	more evar stuff	corbinea	2004-06-28
*	effective evar refining	corbinea	2004-06-26
*	factorisation et generalisation des clauses	barras	2003-11-13
*	petits changements de syntaxe	barras	2003-11-12
*	Added Instantiate ... in	corbinea	2003-11-06
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	backtrack dans l'algo d'unification	barras	2002-04-10
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
*	reparation de make doc (ocamlweb & _)	letouzey	2001-12-19
*	Diverses petites simplications de la machine de preuves.	clrenard	2001-11-19
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	Suppression du retypage dans w_Declare	herbelin	2001-09-09
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Documentation	herbelin	2000-12-18
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Nettoyage de l'interface de Pfedit	herbelin	2000-05-04
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	- environment -> safe_environment	filliatr	1999-12-01
*	- documentation repertoire proofs/	filliatr	1999-10-20