coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	+ Debugging and cleaning functional principle generation tactic	jforest	2006-03-14
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
*	Julien:	bertot	2006-02-22
*	bug correction	bertot	2006-02-17
*	Julien:	bertot	2006-02-17
*	securing intros (we now use h_intro)	bertot	2006-02-09
*	Minor bugs fixes	bertot	2006-02-09
*	Changing Set to Type for iter.	bertot	2006-02-08
*	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot	2006-02-08
*	Julien:	bertot	2006-02-08
*	+ Adding an error message when the function cannot be defined	bertot	2006-02-03
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Recursive Definition now supports functions with more than one argument.	coq	2006-01-18
*	Changing well founded induction to fix on accessibility proof in order	bertot	2006-01-12
*	removes several warnings in contrib/interface	bertot	2006-01-11
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	avoids warnings about unused variables	bertot	2005-11-14
*	Adds tools to help in defining new general recursive functions	bertot	2005-11-07