coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-17	Desactivation de la syntaxe v7 de Hint Rewrite en v8	herbelin
2004-03-17	Message d'erreur	herbelin
2004-03-15	bug d'Inversion #529 (pb avec ordre d'evaluation)	barras
2004-03-15	Nouvelle reparation pour Abstract en presence de variables de contexte: on co...	herbelin
2004-03-13	Backtrack sur la réparation de Abstract qui casse autre chose; le problème ...	herbelin
2004-03-12	Retablissement de la correction bug d'inversion faite dans la version 1.116 e...	herbelin
2004-03-12	Ne pas ajouter le contexte de section dans Abstract, il est deja inclus (avec...	herbelin
2004-03-11	code obsolete	herbelin
2004-03-11	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin
2004-03-10	Ajout tactiques stepl et stepr de Nimègue	herbelin
2004-03-10	Correction bug internalisation 'context'	herbelin
2004-03-09	bug de l'inversion (coq-bugs #529)	barras
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'	herbelin
2004-03-01	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin
2004-03-01	Ajout 'replace in'	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-03-01	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-02-26	added breakpoints to help ide	corbinea
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-12	Typo	herbelin
2004-02-12	Plus d'explicitation d'un message d'erreur	herbelin
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin
2004-01-27	Bug (destruct/induction ne savent pas traiter le cas non atomique avec param�...	herbelin
2004-01-23	Bug induction lors de types inductives avec parametres	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2003-12-23	Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...	herbelin
2003-12-23	* empty log message *	barras
2003-12-15	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras
2003-12-13	Correction bug soumis par Yves	herbelin
2003-12-01	Nouvelle tactique EExists	clrenard
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-11-22	Bug introduit avec le 'Simpl f'	herbelin
2003-11-18	Blindage vis a vis des constructeurs partiellement appliques	herbelin
2003-11-17	New tactics : econstructor, eleft, eright, esplit	clrenard
2003-11-15	Bug nommage destruct	herbelin
2003-11-14	Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	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-09	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-08	Code obsolete	herbelin