coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Changement du type d'argument 'TacticArgType X' en un type	herbelin	2006-06-08
*	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin	2006-06-08
*	Factorisation utilisation environnement dans make_pr_tac	herbelin	2006-06-08
*	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin	2006-06-07
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin	2006-05-23
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin	2006-05-19
*	Oubli des symboles du Latin-1	herbelin	2006-05-11
*	Centralisation de la détection lettre/symbole par le lexeur dans les plages ...	herbelin	2006-05-10
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	- Distinction explicite des parties paramètres et arguments dans le type	herbelin	2006-04-27
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin	2006-04-26
*	Diverses corrections de l'afficheur et du traducteur pour s'assurer de	herbelin	2006-04-26
*	Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;	herbelin	2006-04-24
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...	herbelin	2006-03-05
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10