coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Oublié de supprimer du code mort	herbelin	2000-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1171 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ↵	herbelin	2000-12-20
\| \| \| \| \| \|	inductif où la constante la plus proche du Fix est prise en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Elimination du '	delahaye	2000-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring	2000-11-07
\| \| \| \| \| \| \| \| \| \|	de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus besoin de rajouter "Require Plus"	herbelin	2000-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage command -> constr	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	g_natsyntax et g_zsyntax maintenant toujours linkes	filliatr	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commit malencontreux sur précédente version	herbelin	2000-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en conformité nouveau Simpl pour Fix	herbelin	2000-10-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Require Plus ajoute	filliatr	2000-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement nommage des hypothèses; parenthèses pour les tactiques	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parenthèses	herbelin	2000-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	parethèses de tactiques	herbelin	2000-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression doublon	filliatr	2000-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@375 85f007b7-540e-0410-9357-904b9bb8a0f7
*	g_natsyntax.ml	filliatr	2000-03-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@324 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise sous CVS du repertoire theories/Arith	filliatr	2000-03-10
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7