coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression de code mort	notin	2007-02-01
*	Abbreviation of order notation.	msozeau	2007-02-01
*	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea	2007-01-31
*	Fix order of wf and measure arguments, patch Program doc.	msozeau	2007-01-31
*	"suffices" implemented + syntax cleanup	corbinea	2007-01-28
*	decl mode: anonymous facts	corbinea	2007-01-25
*	Correction du bug #1315:	notin	2007-01-22
*	changes in declarative language : by term using tactic	corbinea	2007-01-22
*	Petit oubli dans commit 9474	herbelin	2007-01-11
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	nouvelle indentation des scripts	barras	2006-12-12
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Suite ajout option -output-context	herbelin	2006-12-08
*	Ajout d'une option -output-context qui affiche le contexte en CCI pur à la	herbelin	2006-12-08
*	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin	2006-12-03
*	Correction boucle du parseur en cas de caractÃère non unicode	herbelin	2006-11-20
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	Fichiers obsolètes	herbelin	2006-11-11
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	syntaxe du let in encore	barras	2006-10-31
*	assouplissement de la syntaxe du let de ltac: t1 ; let in autorise	barras	2006-10-31
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	Exports manquants dans ring	barras	2006-10-29
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
*	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin	2006-10-28
*	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin	2006-10-24
*	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin	2006-10-24
*	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin	2006-10-19
*	affichage des ... dans les scripts	barras	2006-10-16
*	Notations:	herbelin	2006-10-09
*	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin	2006-10-03
*	Suppression des lignes vides dans l'affichage des scripts	notin	2006-09-28
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Déplacement surround dans util.ml et parenthésage des déclarations	herbelin	2006-09-23
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin	2006-09-15
*	Ajout possibilité clause "where" dans co-points fixes	herbelin	2006-09-01
*	making otags working	jforest	2006-08-22
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Correction incohérence parsing de %delim dans les motifs	herbelin	2006-07-12
*	Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...	herbelin	2006-07-11
*	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin	2006-07-05
*	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin	2006-07-05
*	Nettoyage code mort	herbelin	2006-07-05
*	Correction typo + ajout Arabic Supplement	herbelin	2006-07-05