coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	this should fix a problem described in a message by Dufourd on July 30th, 2007	bertot	2007-09-06
*	fin de la correction de Function	jforest	2007-08-31
*	correction bug d'efficacite dans Function	jforest	2007-08-31
*	removing a warning at compilation time	jforest	2007-07-13
*	minor bug correction (continuing r 9943)	jforest	2007-07-06
*	Minor bug correction in Function. Non terminating Function e.g.	jforest	2007-07-05
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest	2007-05-17
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...	jforest	2007-04-05
*	correction du bug 1432	jforest	2007-03-11
*	Contounement d'un probleme avec la VM dans Function	jforest	2007-01-26
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	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
*	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