coq - The formal proof system

Age	Commit message (Expand)	Author
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-24	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin
2007-02-16	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau
2007-02-15	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-01	Suppression de code mort	notin
2007-02-01	Abbreviation of order notation.	msozeau
2007-01-31	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea
2007-01-31	Fix order of wf and measure arguments, patch Program doc.	msozeau
2007-01-28	"suffices" implemented + syntax cleanup	corbinea
2007-01-25	decl mode: anonymous facts	corbinea
2007-01-22	Correction du bug #1315:	notin
2007-01-22	changes in declarative language : by term using tactic	corbinea
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