coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin	2010-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles	2007-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10144 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,	notin	2007-06-21
\| \| \| \| \| \| \| \|	et une typo dans Eqdep_deq.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
\| \| \| \| \| \| \|	égalité décidable + maj dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en forme des theories	notin	2006-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modularisation des preuves concernant la logique classique, ↵	herbelin	2006-03-05
\| \| \| \| \| \|	l'indiscernabilité des preuves et l'axiome K git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 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
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5824 85f007b7-540e-0410-9357-904b9bb8a0f7
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵	herbelin	2003-11-29
\| \| \| \| \| \|	par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des dependances dans la tactique Case	mohring	2002-03-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2567 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)	barras	2001-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1790 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise de (*i autour CVS info	mohring	2001-04-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 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
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance ↵	herbelin	2000-03-21
\| \| \| \| \| \|	utilisé par clenv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@344 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntactic Definition n'etaient pas correctemenet importees	filliatr	2000-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@320 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2000-03-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@310 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
	- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7