coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\|
*	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\|
*	Merge PR #6740: Adding a sanity check on inductive variance subtyping.	Maxime Dénès	2018-02-21
\|\
* \|	Adding a test for the construction that was broken in Coccinelle.	Pierre-Marie Pédrot	2018-02-16
\| \| \| \| \| \| \| \| \| \|	There was no test in the test-suite checking for double with-def constraints in module typing.
\| *	Adding a test for variance subtyping in the module system.	Pierre-Marie Pédrot	2018-02-15
\|/
*	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
\| \| \| \| \|	Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\|
*	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \|	Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
*	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \|	We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
*	Unset Asymmetric Patterns	pboutill	2013-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
\| \| \| \| \| \| \|	Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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