coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	bugs avec Pose et Assert	barras	2004-01-09
*	Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...	herbelin	2003-12-23
*	* empty log message *	barras	2003-12-23
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Correction bug soumis par Yves	herbelin	2003-12-13
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Bug introduit avec le 'Simpl f'	herbelin	2003-11-22
*	Blindage vis a vis des constructeurs partiellement appliques	herbelin	2003-11-18
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Bug nommage destruct	herbelin	2003-11-15
*	Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste	herbelin	2003-11-14
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Prise en compte des alias syntaxiques vers des references dans divers lieux d...	herbelin	2003-11-12
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	Traduction semantique des InHyp de clause en InHypValue si local def; simplif...	herbelin	2003-11-09
*	'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...	herbelin	2003-11-09
*	Code obsolete	herbelin	2003-11-08
*	Nettoyage	herbelin	2003-11-08
*	Added Instantiate ... in	corbinea	2003-11-06
*	Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...	herbelin	2003-11-04
*	Bug Double Inversion	herbelin	2003-10-27
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...	herbelin	2003-10-21
*	Correction bug FreshId	herbelin	2003-10-21
*	Globalisation des hints autorewrite	herbelin	2003-10-20
*	Extension de l'utilisation de contradiction	herbelin	2003-10-19
*	Extension de Contradiction au cas d'hypotheses ~A et A dans le contexte	herbelin	2003-10-18
*	subst marche dans les deux sens	filliatr	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...	herbelin	2003-10-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Uniformisation comportement decompEq pour corriger un bug introduit dans le I...	herbelin	2003-10-11
*	Bug calcul du nom de la premiere equation	herbelin	2003-10-11
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
*	Typo	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module'	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...	herbelin	2003-10-10
*	Unification lemInv et lemInv_in	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Bug utilisation nametab pour ltac	herbelin	2003-10-08