coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Applying Tom Prince's patch for build_constant_by_tactic not able to	herbelin	2011-04-08
*	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
*	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill	2010-05-05
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	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
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Changement des named_context	gregoire	2005-12-02
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	Export du type de preuve en cours pour xml	herbelin	2004-03-29
*	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin	2003-10-10
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	simplification common_ancestor	courant	2002-11-13
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Ajout d'un point d'entree pour exporter les arbres de preuves en XML	herbelin	2002-07-24
*	Commentaires	herbelin	2002-06-14
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suite de la suppression : enamed_declaration est remplace par evar_map.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	Transparent	barras	2001-09-20
*	entetes	filliatr	2001-03-15
*	exporting traverse_to and mutate: they are used in pcoq.	bertot	2001-02-08
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	Renommage canonique :	herbelin	2000-10-18
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Déplacement de save_thm and co de PFedit vers Command	herbelin	2000-05-25
*	Doc	herbelin	2000-05-23
*	doc	herbelin	2000-05-18
*	Achèvement nettoyage Pfedit	herbelin	2000-05-05
*	Nettoyage de l'interface de Pfedit	herbelin	2000-05-04
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	- erreurs Pretype	filliatr	1999-12-10
*	debug reset	filliatr	1999-12-10
*	premier debugage	filliatr	1999-12-05
*	modules profile, Coqinit et Coqtop (=main)	filliatr	1999-12-03