coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...	herbelin	2006-07-04
*	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin	2006-07-03
*	Mise à jour (avec retard) des niveaux de la table default_pattern_levels	herbelin	2006-07-03
*	Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT E...	herbelin	2006-06-23
*	Suppresion redondance interp_entry_name entre Q_util et Argextend	herbelin	2006-06-23
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
*	Bug is_number	herbelin	2006-06-10
*	Plus de Declare Module sans vrai type explicite	herbelin	2006-06-08