coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
\| \| \| \| \| \| \| \| \|	Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 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
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 ↵	soubiran	2007-05-25
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran	2007-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des univers algébriques dans les types inférés dans	herbelin	2007-01-19
\| \| \| \| \| \| \| \| \|	les interfaces de module (bug similaire à #1302 mais pour les définitions -- au lieu des inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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
*	remplacement d'un test d'egalite par un test de convertibilite dans ↵	jforest	2006-12-22
\| \| \| \| \| \|	injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarification des contraintes sur le contexte de paramètres des	herbelin	2006-10-17
\| \| \| \| \| \| \| \| \| \| \|	inductifs dans le test de sous-typage (exigence du même nombre d'arguments uniformes attendus mais pas d'exigence spéciale sur les définitions locales du contexte à partir du moment où les types et constructeurs sont convertibles quand généralisés par rapport au contexte de paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9247 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
\| \| \| \| \| \| \| \|	vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug #1242) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1181	jforest	2006-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9138 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Conformité nouveaux principes: Declare Module non utilisable pour définir ↵	herbelin	2006-05-10
\| \| \| \| \| \|	un module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test synchronisation chargement objets non logiques	herbelin	2006-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8719 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
*	MAJ syntaxe v7 avant activation en syntaxe v8	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7689 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Anciennement déplacé dans 'output'	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplest Demo on modules	coq	2003-11-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
*	L'exemple phare de modules - simplifie pour TPHOLs	coq	2003-09-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrige Bug (PR#290)	coq	2003-05-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commentaire	coq	2003-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3667 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout	coq	2003-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-11-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Encore quelques tests sur modules...	coq	2002-08-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2970 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petites corrections ici et la	coq	2002-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7