coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	* empty log message *	barras	2003-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8451 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Aspect mathematique de Coq	herbelin	2003-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Qques avancees sur la doc des scopes	herbelin	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout intro-pattern des inductifs unaire	herbelin	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8445 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8444 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ Reset Initial	herbelin	2003-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amendements apres lecture Bruno	herbelin	2003-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout projections; reparation script coq	herbelin	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8440 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Conjecture	herbelin	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout Admitted	herbelin	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout symmetry in; NArithRing; Hint Local; MAJ V8; typos	herbelin	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour Cases	mohring	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8436 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	mohring	2003-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8432 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	relecture v8	herbelin	2003-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ ltac, INSTALL, typos	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8429 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour V8	mohring	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8428 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typos	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de la grammaire des intro-patterns	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation 'inversion as'	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8424 85f007b7-540e-0410-9357-904b9bb8a0f7
*	des %N inutiles et les messages d'erreurs n'aparaissent plus dans la doc	barras	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement du chap sur ltac	barras	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	v8/CIC	mohring	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise a jour V8	mohring	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petits changements dans la doc de functional scheme et functional induction.	coq	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COQBIN plus necessaire, typos	marche	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8417 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oups	filliatr	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	passe sur les labels et les refs dans chapitres tactiques	filliatr	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8414 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour CIC	mohring	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc proof with	narboux	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8411 85f007b7-540e-0410-9357-904b9bb8a0f7
*	avancement	clrenard	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8410 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj V8	filliatr	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8409 85f007b7-540e-0410-9357-904b9bb8a0f7
*	premiere passe V8	filliatr	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore un peu de tactiques...	filliatr	2003-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8407 85f007b7-540e-0410-9357-904b9bb8a0f7
*	encore un peu de tactiques...	filliatr	2003-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	doc de ltac faite	barras	2003-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ induction/destruct/simpl	herbelin	2003-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide menus on golas	marche	2003-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8403 85f007b7-540e-0410-9357-904b9bb8a0f7
*	tactiques	filliatr	2003-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8402 85f007b7-540e-0410-9357-904b9bb8a0f7