coq - The formal proof system

Age	Commit message (Collapse)	Author
2003-03-31	Ajout d'un message à FailTac	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31	Correcting a bug occuring when the mimicked function had a	courtieu
	lambda-abstraction inside a Cases. I had to make the term of the induction principle a bit less clean (more eta expansions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-01	Added some tests to make more robust the tactique "Functional	courtieu
	Induction". Namely: check that the given function is a really a constant, and check that the number of given argument is exactly the arity of the given function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27	Adding tests for the "functional induction" facility.	bertot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot
	for recursive functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3710 85f007b7-540e-0410-9357-904b9bb8a0f7