coq - The formal proof system

Age	Commit message (Expand)	Author
2002-06-19	Coercion de la syntaxe des motifs non atomiques	herbelin
2002-06-18	coq_makefile utilise maintenant coqdoc	filliatr
2002-06-17	Suppression de fct_eq	desmettr
2002-06-17	Prise en compte de exp, cosh et sinh	desmettr
2002-06-17	Modifications relatives a l'ajout de Rtrigo_def	desmettr
2002-06-17	Definitions de exp, cos et sin	desmettr
2002-06-17	* empty log message *	desmettr
2002-06-14	* empty log message *	herbelin
2002-06-14	Commentaires	herbelin
2002-06-14	* empty log message *	herbelin
2002-06-13	Bug non vérification non redondance par Cut	herbelin
2002-06-13	Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin
2002-06-13	Ajout map_inductive_type et map_ind_family	herbelin
2002-06-13	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-11	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-07	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-06	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-05	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-04	* empty log message *	courant
2002-06-04	'make check' echoue si au moins un test echoue.	courant
2002-06-03	* 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-05-31	Les VContext ne sont plus des fermetures (temporaire)	delahaye
2002-05-31	Ajout d'occurrences de Field (ne pas enlever)	delahaye