coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Gestion des arguments implicites dans les Functions bien fondees	jforest	2006-09-19
*	correction of bug #1220	jforest	2006-09-18
*	Message modification in Function	jforest	2006-09-16
*	Minor bug correction in well-founded Function.	jforest	2006-09-15
*	two minor bug corrections in General Recursive Functions	jforest	2006-08-25
*	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest	2006-08-16
*	Bug corrections in Function.	jforest	2006-08-11
*	In the old version, recursive functions cannot be declared inside a section	bertot	2006-08-08
*	removing a warning	jforest	2006-05-26
*	Error during last commit (coq didn't compile)	jforest	2006-05-23
*	cleanning code	jforest	2006-05-23
*	Correcting a bug in identifiers manipulation	jforest	2006-05-22
*	Correcting an old bug during generation of generale recursive functions.	jforest	2006-05-09
*	+ correcting a bug in general recursive function (match e with _ => match f e...	jforest	2006-05-07
*	Fixing two minor bugs in recdef and graph of function generation.	jforest	2006-05-03
*	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest	2006-05-03
*	If function creates proof obligation, there are now printed once.	courtieu	2006-04-28
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	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