coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Test de l'interprétation des fermetures de Match Context	herbelin	2002-06-13
*	Réparation de l'interprétation des fermetures (sans casser Field!)	herbelin	2002-06-13
*	Petits beug d'affichages.	gregoire	2002-06-13
*	Tests pour la tactique Reg	desmettr	2002-06-11
*	* empty log message *	desmettr	2002-06-11
*	* empty log message *	desmettr	2002-06-11
*	Ranalysis.v	desmettr	2002-06-11
*	L'ordre supérieur avait quelque peu été oublié dans l'unification...	herbelin	2002-06-07
*	extraction vers scheme	letouzey	2002-06-07
*	Adding file theories/ZArith/Zsqrt.v that contains a square root function.	bertot	2002-06-07
*	Ajout de FNL ou utilisation de msgnl	herbelin	2002-06-07
*	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin	2002-06-07
*	I added a comment on the tactic compute_POS.	bertot	2002-06-07
*	This example does not work in coq-7.3, but does in coq-7.2.	bertot	2002-06-07
*	Ajout coercion constr vers hyp quantifiée	herbelin	2002-06-06
*	Ajout exemple JCF conflit variable interne, variable de section	herbelin	2002-06-06
*	Tentative de réparation d'un bug Omega: une variable de section qui après e...	herbelin	2002-06-06
*	Des exemples sérieux	herbelin	2002-06-06
*	Passage de PatternMatchingFailure vers UserError pour capture par tclFIRST	herbelin	2002-06-06
*	Correction non reconnaissance des variables de section dans les afficheurs de...	herbelin	2002-06-06
*	Ajout exemple Yves renommage différent d'une var de section	herbelin	2002-06-06
*	affaiblissement hyp de Zmult_reg_left	filliatr	2002-06-05
*	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin	2002-06-05
*	Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotification	herbelin	2002-06-05
*	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin	2002-06-05
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin	2002-06-05
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	* empty log message *	courant	2002-06-04
*	'make check' echoue si au moins un test echoue.	courant	2002-06-04
*	* empty log message *	herbelin	2002-06-03
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
*	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin	2002-06-03
*	Factorisation de 'Show Programs' au premier niveau de Vernac_.command	herbelin	2002-06-03
*	Les VContext ne sont plus des fermetures (temporaire)	delahaye	2002-05-31
*	Ajout d'occurrences de Field (ne pas enlever)	delahaye	2002-05-31
*	.depend.coq remis a jour	letouzey	2002-05-31
*	Ajout des -I contrib	herbelin	2002-05-30
*	Nettoyage	herbelin	2002-05-30
*	Mise au point de declare_red_expr	herbelin	2002-05-30
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	syntax/PPTactic.v passe au niveau ML	herbelin	2002-05-29
*	Déplacement de proofs vers tactics	herbelin	2002-05-29
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Introduction de syntaxe convivial +,*,<=,<,>=	herbelin	2002-05-29
*	Double Induction prend maintenant des noms d'hyppthèses	herbelin	2002-05-29
*	Utilisation d'Infix/Distfix autant que possible	herbelin	2002-05-29
*	Contournement des My_special_variable	herbelin	2002-05-29
*	* empty log message *	herbelin	2002-05-29