coq - The formal proof system

Age	Commit message (Collapse)	Author
2010-06-03	plugin groebner updated and renamed as nsatz; first version of the doc of ↵	pottier
	nsatz in the refman git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13056 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19	Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey
	The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-16	nouvelle version de la tactique groebner proposee par Loic:	barras
	- algo de Janet (finalement pas utilise) - le hash-cons des certificats de Benjamin et Laurent pas encore integre - traitement des puissances jusqu'a 6 (methode totalement naive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12088 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7