coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Branchement sur nouvelle interface de declare_numeral_interpreter	herbelin	2006-02-04
*	Recherche des global_reference paresseusement pour pouvoir interpréter	herbelin	2006-02-04
*	parsing/g_ascii_syntax.ml	herbelin	2006-02-04
*	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin	2006-01-31
*	Ajout syntaxe concrète Proposition, synonyme de Lemma	herbelin	2006-01-29
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin	2006-01-28
*	Correction bug Inspect introduit par le passage du discharge à une méthode ...	herbelin	2006-01-28
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin	2006-01-28