coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	maj	filliatr	2004-10-26
*	maj	filliatr	2004-10-25
*	Word "setoid" banned from the error messages. "relation" used instead.	sacerdot	2004-10-25
*	Added option -no-vm.	sacerdot	2004-10-25
*	Missing check implemented (closes a bug from Bas Spitters).	sacerdot	2004-10-25
*	maj	filliatr	2004-10-24
*	maj	filliatr	2004-10-22
*	maj	filliatr	2004-10-21
*	The morphism lemma type was simplified only in modules and not in module	sacerdot	2004-10-21
*	Error message improved.	sacerdot	2004-10-21
*	maj	filliatr	2004-10-20
*	maj	filliatr	2004-10-20
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)	barras	2004-10-20
*	The bug already closed in revision 1.90 was reintroduced again.	sacerdot	2004-10-20
*	maj	filliatr	2004-10-19
*	Proof term size reduction (again).	sacerdot	2004-10-19
*	maj	filliatr	2004-10-18