coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Code mort	herbelin	2004-11-22
*	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin	2004-11-22
*	Réparation incompatibilité de comportement introduite lors de mise en compa...	herbelin	2004-11-22
*	compatibility with POWERPC	gregoire	2004-11-22
*	Expansion Case dans injection et discriminate (cf bug #829)	herbelin	2004-11-21
*	'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marche	herbelin	2004-11-20
*	Généralisation à Type de certaines propriétés des relations	herbelin	2004-11-19
*	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin	2004-11-19
*	When a reference to a constructor is met its inductive type must be closed.	sacerdot	2004-11-18
*	Code mort	herbelin	2004-11-18
*	Locate Module	herbelin	2004-11-17
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	bug module with ... + vm	barras	2004-11-17
*	Mise en page	herbelin	2004-11-17
*	bug module M:=N avec vm	barras	2004-11-17
*	Ajout 'Locate Module'	herbelin	2004-11-17
*	Bug 'Locate Library lib' quand 'lib' est aussi un module	herbelin	2004-11-17
*	Déclaration de '..' comme mot-clé (résoud bug #856)	herbelin	2004-11-17
*	Message d'erreur	herbelin	2004-11-17
*	Suppression capture des variables par lieurs non liés dans Notation; simplif...	herbelin	2004-11-17
*	Suppression capture des variables par lieurs non liés dans Notation	herbelin	2004-11-17
*	Test lieurs dans Notation	herbelin	2004-11-17
*	test-suite/output/Notations.out	herbelin	2004-11-17
*	Copy of the definition of prodT (already in the standard library) removed.	sacerdot	2004-11-16
*	dead (and obsolete) code (in comments) removed	sacerdot	2004-11-16
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	bug coqmktop avec libcoqrun.a en bytecode	barras	2004-11-15
*	Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...	herbelin	2004-11-15
*	* empty log message *	gregoire	2004-11-12
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Correction bug #868	herbelin	2004-11-10
*	MAJ	herbelin	2004-11-09
*	code mort	herbelin	2004-11-09
*	Prise en compte des notations récursives dans l'option 'format'	herbelin	2004-11-08
*	MAJ commentaire sur incohérence EM dans Set	herbelin	2004-11-07
*	autorewrite moved from HIGHTACTICS to TACTICS (to implement Printing	sacerdot	2004-11-05
*	Univ.pr_univ ==> Univ.pr_uni	sacerdot	2004-11-04
*	Affichage des univers	herbelin	2004-11-04
*	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin	2004-11-02
*	qq bugs du highlight de CoqIDE	filliatr	2004-10-28
*	Added code to get rid of duplicate rewriting rules.	sacerdot	2004-10-28
*	Ajout 'dependent rewrite in'	herbelin	2004-10-28
*	maj	filliatr	2004-10-27
*	Factorisation cut_replacing	herbelin	2004-10-27
*	Restructuration fonctions de réécriture depuis égalité dépendante	herbelin	2004-10-27
*	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin	2004-10-27
*	Ajout test dependent rewrite	herbelin	2004-10-27
*	Bug mauvais nom d'entrée binder_constr quand récursion gauche	herbelin	2004-10-27
*	Non affichage des notations réduites à une variable	herbelin	2004-10-27