coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-24	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-19	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin
2006-10-16	affichage des ... dans les scripts	barras
2006-10-09	Notations:	herbelin
2006-10-03	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin
2006-09-28	Suppression des lignes vides dans l'affichage des scripts	notin
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-23	Déplacement surround dans util.ml et parenthésage des déclarations	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-15	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin
2006-08-22	making otags working	jforest
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2006-07-12	Correction incohérence parsing de %delim dans les motifs	herbelin
2006-07-11	Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...	herbelin
2006-07-05	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-04	Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...	herbelin
2006-07-03	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-06-23	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-22	Added {measure x f} as a valid recursion order.	msozeau
2006-06-10	Bug is_number	herbelin
2006-06-08	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-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-23	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-19	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin
2006-05-11	Oubli des symboles du Latin-1	herbelin
2006-05-10	Centralisation de la détection lettre/symbole par le lexeur dans les plages ...	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	- 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-26	- 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-24	Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau