coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-27	Cette dérivation de paradoxe passait en V8.1beta	herbelin
2006-10-27	Restriction au implémenteurs	herbelin
2006-10-27	Ajout ListTactics	herbelin
2006-10-27	Ajout ListTactics	herbelin
2006-10-26	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin
2006-10-26	Affichage d'un message d'erreur losque qu'une relation n'a pas été déclar�...	notin
2006-10-26	Noms de compatibilité déplacés en bloc à la fin du fichier	herbelin
2006-10-26	Some fixes in experimental merging of two functional graphs.	courtieu
2006-10-26	added doc for declarative language	corbinea
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-26	Facilities to automatically solve obligations	msozeau
2006-10-26	MAJ crédits, fresh; documentation apply in	herbelin
2006-10-26	MAJ	herbelin
2006-10-26	Petit bug apply in	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-10-25	Suite commit 9277	herbelin
2006-10-25	oups, ne chargeait pas les bons fichiers	letouzey
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-25	coqdep -slash	barras
2006-10-25	Ménage	notin
2006-10-25	oops	barras
2006-10-25	conflit de nom (Field_theory) modulo la casse	barras
2006-10-24	Extension de fresh (suite)	herbelin
2006-10-24	Changement de la valeur par défaut de with_geoproof (stabilité coqide)	notin
2006-10-24	Test apply in	herbelin
2006-10-24	Insère une coercion vers Sortclass dans 'contradiction' si nécessaire	herbelin
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-24	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-10-24	Hack peu élégant pour permettre de parser des listes avec séparateurs dans	herbelin
2006-10-24	Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...	herbelin
2006-10-23	fixed same_file (#1141)	barras
2006-10-23	fixed non-bug #1213	barras
2006-10-23	bug #1194: normalisation evars a la sortie de focus	barras
2006-10-23	Fixed "Show intros" which did not look at hypothesis.	courtieu
2006-10-23	Add a flush after backtracking x y z and before printing subgoals.	courtieu
2006-10-23	Add a flush for a warning.	courtieu
2006-10-21	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin
2006-10-21	Pas d'@ dans les identificateurs (pour F4 and co)	herbelin
2006-10-21	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin
2006-10-20	MAJ	herbelin
2006-10-20	Correction du bug #1255 (réécriture setoid sous un produit)	notin
2006-10-20	Correction de la localisation des erreurs en interactif (numéro de	herbelin
2006-10-20	Starting to add a function schemes merging command (not finished, not	courtieu
2006-10-19	Correction sym -> comm	herbelin
2006-10-19	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin
2006-10-17	field_simplify_eq profite de la factorisation de Laurent	barras
2006-10-17	Clarification des contraintes sur le contexte de paramètres des	herbelin
2006-10-17	Noms "canoniques" pour certaines des propriétés de xor.	herbelin
2006-10-17	Mise en forme des theories	notin