coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Congruence: Fixing a bug with native projections.	Hugo Herbelin	2018-03-27
\| \| \| \| \| \| \| \| \|	There is a code to turn constants denoting projections into proper primitive projections, but it did not drop parameters. The code seems anyway redundant with an "expand_projections" which is already present in Cctac.decompose_term. After removal of this code, the two calls to congruence added to cc.v work.
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\
\| *	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
\| \| \| \| \| \| \| \| \| \| \| \|	Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
* \|	Using build_selector from Equality as a replacement of the selector	Hugo Herbelin	2016-03-05
\|/ \| \| \| \| \| \| \|	in cctac which does not support indices properly. Incidentally, this should fix a failure in RelationAlgebra, where making prod_applist more robust (e8c47b652) revealed the discriminate bug in congruence.
*	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
\|
*	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
*	congruence now knows about _ -> _	corbinea	2008-02-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10579 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1679 (congruence) et ajout test-suite	corbinea	2007-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 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
*	Suppression test CCSolve car remplaçé par Congruence mais qui ne traite ↵	herbelin	2005-09-09
\| \| \| \| \| \|	pas les connecteurs propositionnels (pour Pierre C.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7359 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	removal of CC.v lemata in cc (deprecated)	corbinea	2003-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CC: added injection theory	corbinea	2003-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7