coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:	sacerdot	2004-07-23
*	Since setoid_{replace,rewrite} now uses replace there is a circularity	sacerdot	2004-07-23
*	Setoid_replace.setoid_replace last argument (that was supposed to be always	sacerdot	2004-07-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	syntax compatibility fix	corbinea	2004-07-02
*	instantiate entry: constr -> lconstr	corbinea	2004-06-30
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Ajout de la coercion id dans context vers evaluable constant (bug #777)	herbelin	2004-06-28
*	effective evar refining	corbinea	2004-06-26
*	bug #787 de Roland	barras	2004-06-02
*	Clarify the distinction between quantified_hypothesis and declared_or_quantif...	herbelin	2004-06-02
*	Bug mauvais sigma	herbelin	2004-05-07
*	Terminologie plus intuitive: evaluable -> unfoldable	herbelin	2004-04-30
*	Morphismes déclarés comme Lemma pas comme Definition	herbelin	2004-03-31
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Backtrack sur commit 1.20	herbelin	2004-03-18
*	Desactivation de la syntaxe v7 de Hint Rewrite en v8	herbelin	2004-03-17
*	Message d'erreur	herbelin	2004-03-17
*	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-15
*	Backtrack sur la réparation de Abstract qui casse autre chose; le problème ...	herbelin	2004-03-13
*	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-12
*	code obsolete	herbelin	2004-03-11
*	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin	2004-03-11
*	Ajout tactiques stepl et stepr de Nimègue	herbelin	2004-03-10
*	Correction bug internalisation 'context'	herbelin	2004-03-10
*	bug de l'inversion (coq-bugs #529)	barras	2004-03-09
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	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-02
*	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-03-01
*	added breakpoints to help ide	corbinea	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	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-02-12
*	Bug (destruct/induction ne savent pas traiter le cas non atomique avec param�...	herbelin	2004-01-27
*	Bug induction lors de types inductives avec parametres	herbelin	2004-01-23
*	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