coq - The formal proof system

Age	Commit message (Expand)	Author
2007-01-11	Petit oubli dans commit 9474	herbelin
2007-01-10	Merge from Lionel Elie Mamane's private branch:	lmamane
2007-01-10	Nouvelle approche pour le discharge modulaire	herbelin
2006-12-23	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau
2006-12-12	nouvelle indentation des scripts	barras
2006-12-11	Changement dans le kernel :	bgregoir
2006-12-08	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-03	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin
2006-11-20	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-17	The emacs-U option now does not output any char above 250.	courtieu
2006-11-11	Fichiers obsolètes	herbelin
2006-11-02	gestion speciale du niveau 5 des ltac	barras
2006-10-31	syntaxe du let in encore	barras
2006-10-31	assouplissement de la syntaxe du let de ltac: t1 ; let in autorise	barras
2006-10-30	fixed field_simplify + changed precedence of let and fun in ltac	barras
2006-10-29	Exports manquants dans ring	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	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-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