coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
\| \| \| \| \| \| \| \| \|	arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct handling of existential variables when multiple different	msozeau	2011-02-08
\| \| \| \| \| \| \| \| \|	instances of the lemma are rewritten at once. Cleanup dead code and put the problematic cases in the test-suite. Also fix some test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug using explictly declared implicit arguments in inductive arities.	herbelin	2010-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export definition of type implicits_list for contribs + fixed a	herbelin	2010-10-05
\| \| \| \| \| \| \|	discharge bug of implicit arguments related to commit 13484 (multiple implicit arguments sequences patch). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bugs in previous commits about implicit arguments:	herbelin	2010-10-04
\| \| \| \| \| \| \| \| \|	- fixing r13483 (supposed dead code in impargs was actually half-living: implicit arguments mode should merge with the {...} manually given implicit arguments but not with the "Implicit Arguments [...]" arguments), - fixing code of drop_first_implicits in r13484. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
\| \| \| \| \| \| \| \| \|	Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revision 12439 continued, printing part (notations to names behave	herbelin	2009-10-29
\| \| \| \| \| \| \| \|	like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Local/Global revision 12418 continued	herbelin	2009-10-26
\| \| \| \| \| \| \| \|	- Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 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
*	Correction bug calcul des implicites en présence d'evars dans les types	herbelin	2007-05-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9827 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin	2006-09-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Relâchement de l'exigence que les types des paramètres et le type des (co-)points fixes soient donnés. Ils peuvent maintenant être inférés à partir des autres informations de types. - Plus de déclaration séparée de celles des fonctions d'un bloc de points fixes qui n'interviennent pas dans la définition des autres (collect_non_rec): remplacement par un simple warning en cas de non dépendance mutuelle de toutes les fonctions du bloc (de toutes façons les fonctions qui intervenaient dans les autres sans en dépendre - càd les fonctions définissables avant la partie point fixe - n'étaient pas détectées) - Ajout du test de dépendance mutuel au cas des co-points fixes Extension et réorganisation de l'interprétation des blocs de définitions (co-)inductives: relâchement de l'exigence que les types des paramètres soient donnés. Ils peuvent maintenant être inférés à partir des autres informations des blocs d'inductifs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 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
*	Corrections	herbelin	2004-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exemple de Frederic	herbelin	2004-02-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Niveau V8	herbelin	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fermeture de la section maintenant necessaire	herbelin	2003-11-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un exemple de Christine	herbelin	2001-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2001-12-13
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7