coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Code mort	herbelin	2001-08-05
*	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin	2001-08-05
*	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin	2001-08-05
*	Ajout error_global_not_found	herbelin	2001-08-05
*	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin	2001-08-05
*	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin	2001-08-05
*	Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...	herbelin	2001-08-05
*	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin	2001-08-05
*	Nouveau profiler compatible avec ocaml >= 3.01	herbelin	2001-08-05
*	Ajout code pour un Destruct similaire au NewInduction	herbelin	2001-08-01
*	Ajout make_elimination_ident	herbelin	2001-08-01
*	Ajout add_prefix/add_suffix	herbelin	2001-08-01
*	Ajout profile dans PARSERREQUIRE, nécessaire si certaines fonctions d'un des...	herbelin	2001-08-01
*	MAJ vis à vis de ocaml 3.01	herbelin	2001-08-01
*	Suppression de l'affichage du non-reparsable 'Local constraint change'	herbelin	2001-07-24
*	Bug Simpl	herbelin	2001-07-24
*	Comentaire errone.	clrenard	2001-07-23
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Nettoyage	herbelin	2001-07-21
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Changements dans le traitement des qualid's	delahaye	2001-07-19
*	modifs de preuves (plus simples)	mayero	2001-07-19
*	Ajout de la contrib sur les graphes	mohring	2001-07-18
*	"make clean" nettoie les .g all.ps all-gal.ps et les fichiers HTML	filliatr	2001-07-17
*	all.g.ps -> all-gal.ps	filliatr	2001-07-16
*	compat -sort et -suffix	filliatr	2001-07-16
*	cibles all.ps et all-gal.ps (utilisation de coqweb)	filliatr	2001-07-16
*	utilisation de printf (simplif)	filliatr	2001-07-16
*	modif Map section	mohring	2001-07-16
*	Nettoyage	mohring	2001-07-16
*	reparation regles pour parsing Coercion Local	mohring	2001-07-13
*	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...	herbelin	2001-07-13
*	Setoid_rewrite -> Rewrite	clrenard	2001-07-10
*	Branchement sur bad_tactic_args	herbelin	2001-07-10
*	Branchement sur bad_tactic_args	herbelin	2001-07-10
*	Ajout des fichiers pour le Ring pour setoides	clrenard	2001-07-10
*	Ajout du .ml pour la tactique Setoid_replace	clrenard	2001-07-10
*	Ajout du .v pour la tactique Setoid_replace	clrenard	2001-07-10
*	Changement de place de la tactique Setoid_rewrite et renommage	clrenard	2001-07-10
*	Changement de place de la tactique Setoid_rewrite	clrenard	2001-07-10
*	Ajout d'un Ring pour setoides	clrenard	2001-07-10
*	Changement de place et de nom de la tactique Setoid_rewrite.	clrenard	2001-07-10
*	anomaly -> error	clrenard	2001-07-10
*	MAJ de la MAJ	herbelin	2001-07-09
*	MAJ	herbelin	2001-07-09
*	Backtrack sur le warning Require en Section: trop contraignant	herbelin	2001-07-09
*	Les tables de coercions ne doivent pas survivre aux sections	herbelin	2001-07-06
*	la conversion ne doit être testé dans evar_conv qu'en absence de evar	herbelin	2001-07-06
*	has_undefined_isevars était buggé	herbelin	2001-07-06
*	version 7.0+1 (pour Nicolas Magaud)	filliatr	2001-07-06