coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Correction bug #1302	herbelin	2007-01-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test condition de garde	barras	2006-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Check that sort-polymorphic inductive types is not too lax	herbelin	2006-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9297 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cette dérivation de paradoxe passait en V8.1beta	herbelin	2006-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9294 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adaptation des tests suite à la modification de Rewrite .. in (r9201)	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9239 85f007b7-540e-0410-9357-904b9bb8a0f7
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
\| \| \| \| \| \| \| \| \| \| \| \|	InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stricte positivité en présence de types inductifs imbriqués avec ↵	herbelin	2006-06-23
\| \| \| \| \| \|	paramètres récursivement non uniformes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deux vérifications que le polymorphisme de sorte des inductifs ne ↵	herbelin	2006-06-22
\| \| \| \| \| \|	fonctionne pas incorrectement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction trou de typage des éliminations d'inductifs introduit dans ↵	herbelin	2006-05-13
\| \| \| \| \| \|	commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cf ltac4.v	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement params_ind	mohring	2005-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-suite/output/Notations.out	herbelin	2004-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2004-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6225 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
\| \| \| \| \| \| \|	reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cacher les .v8	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4558 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test d'implicite incorrect depuis que eq porte sur Type	barras	2003-09-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2003-01-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tests ltac	herbelin	2003-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test for redundant clauses	herbelin	2002-08-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2968 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin	2002-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-04-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2638 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Sur l'exahustivité du filtrage	herbelin	2001-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2224 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test soumis par Randy Pollack	herbelin	2001-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2131 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test de dépendances de ClearBody	herbelin	2001-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quelques signes extérieurs de la sémantique de Remark, question visibilité	herbelin	2001-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tests l'incohérence des univers	herbelin	2001-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2001-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1705 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Erreurs de Cases	mohring	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'erreurs sur le Case avec branche redondante	mohring	2001-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1645 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de tests	mohring	2001-04-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1586 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2001-03-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas d'Apply dans Tauto	delahaye	2001-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du test de Tauto	delahaye	2001-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de tests	mohring	2000-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1087 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tests automatiques	herbelin	2000-12-09
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1082 85f007b7-540e-0410-9357-904b9bb8a0f7