coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression du retypage dans w_Declare	herbelin	2001-09-09
*	MAJ	herbelin	2001-09-09
*	Tests l'incohérence des univers	herbelin	2001-09-09
*	MAJ	herbelin	2001-09-08
*	MAJ	herbelin	2001-09-07
*	Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)	herbelin	2001-09-07
*	Suppression des library roots, on teste si un nom est absolu autrement	herbelin	2001-09-07
*	Rétablissement de Print Section	herbelin	2001-09-06
*	MAJ	herbelin	2001-09-06
*	Bug default module name (2eme)	herbelin	2001-09-06
*	Bug default module name	herbelin	2001-09-06
*	Version de la reduction dans Closure plus econome en memoire:	barras	2001-09-05
*	Nouveau coq.spec avec les droits de root	herbelin	2001-09-04
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
*	Correction d'un bug de pretty-print.	clrenard	2001-09-03
*	prise en compte de Load par coqdep	filliatr	2001-08-31
*	Fin de la modif Exc/option	mohring	2001-08-30
*	ajout option , Exc --> option, et lemmes dans les theories	mohring	2001-08-29
*	Change la constante d'entree de Immediate	mohring	2001-08-28
*	Remplace numarg -> pure_numarg dans Double Induction	mohring	2001-08-28
*	remplace numarg -> pure_numarg	mohring	2001-08-28
*	Rétablissement nom de section Map après résolution bugs surcharge de noms	herbelin	2001-08-13
*	Protection des commentaires pour coqtex et coqweb	herbelin	2001-08-13
*	bug de Bruijn	herbelin	2001-08-13
*	bug incompatibilité	herbelin	2001-08-13
*	Pour contourner un bug de camlp4 3.02	herbelin	2001-08-10
*	Hack rapide pour réduire significativement la taille des vo	herbelin	2001-08-10
*	Bug	herbelin	2001-08-10
*	Prsing	herbelin	2001-08-10
*	Prise en compte des strings et des flottants dans les statistiques de tailles...	herbelin	2001-08-10
*	Parsing	herbelin	2001-08-10
*	Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVE	herbelin	2001-08-10
*	Renommage TrueCut -> Assert	herbelin	2001-08-08
*	Ajout nf_betaiota dans le cut interne	herbelin	2001-08-08
*	La grammaire n'était plus LL1	herbelin	2001-08-08
*	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant	2001-08-08
*	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin	2001-08-07
*	Passage au nouveau Destruct	herbelin	2001-08-07
*	Nouvelle entrée ident_or_numarg	herbelin	2001-08-06
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	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