coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-21	Renommage Implicits -> Implicit	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-21	Renommages divers.	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-21	Parsing au niveau lconstr des patterns de 'match context'	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-21	Conflit de nom Pplus dans positive et dans polynomial (de ring)	herbelin
2003-09-21	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin
2003-09-21	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin
2003-09-21	Nettoyage	herbelin
2003-09-19	coqide auto complete initial bug fix	marche
2003-09-19	Coqide : les nouveaute d'aout	monate
2003-09-19	'::' est deja pris en V7	herbelin
2003-09-19	maj	filliatr
2003-09-19	Section et report Infix hors section	herbelin
2003-09-19	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...	herbelin
2003-09-19	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin
2003-09-19	Ajout notation :: pour cons	herbelin
2003-09-19	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin
2003-09-19	parsing	herbelin
2003-09-18	Interface Eauto	herbelin
2003-09-18	Traduction de Instantiate	herbelin
2003-09-18	Niveau du 'as' des motifs	herbelin
2003-09-18	Traduction de '_' comme reference	herbelin
2003-09-18	Parsing correct des explicites en cas de projection	herbelin
2003-09-18	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin
2003-09-18	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin
2003-09-18	Simplification afficheur de tactiques non primitive	herbelin
2003-09-18	bug fix: term reduced in bad env	barras
2003-09-17	maj	filliatr
2003-09-16	En attendant l'afficheur...	herbelin
2003-09-16	Pour appliquer les noms reserves aussi aux binders	herbelin
2003-09-16	Pour cacher le contenu de Load au traducteur	herbelin
2003-09-16	Tentative amelioration pretty-printing symboles	herbelin
2003-09-16	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...	herbelin
2003-09-16	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)	herbelin
2003-09-15	Reprise de coqbinaries dans translation	herbelin
2003-09-14	Bug PR#324	herbelin
2003-09-13	Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisie	herbelin
2003-09-13	Deplacement de Declare vers Termops	herbelin
2003-09-13	maj	filliatr
2003-09-12	Retour à des cibles plus explicites: world7 et world8, install7 et install8	herbelin
2003-09-12	Outil de test de la traduction et de la compilation en v8 sans modification des	herbelin
2003-09-12	Ajout install7 et coqwc dans tools	herbelin
2003-09-12	Ajout cible world7	herbelin
2003-09-12	Divers	herbelin
2003-09-12	Ajout nouvelles commandes	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin