coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Correction in generate_graph (now handles fun _ => fix ....)	jforest	2006-05-05
*	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
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
*	If function creates proof obligation, there are now printed once.	courtieu	2006-04-28
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	- Distinction explicite des parties paramètres et arguments dans le type	herbelin	2006-04-27
*	Message d'erreur plus informatif	herbelin	2006-04-27
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24
*	decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)	letouzey	2006-04-20
*	Added code to support "Program Lemma/Example... etc"	msozeau	2006-04-16
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	Test files for subtac.	msozeau	2006-04-14
*	Simplifying the proof of principles	jforest	2006-04-12
*	Fixes for new unification, not used in default version as it really changes u...	msozeau	2006-04-10
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau	2006-04-10
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	appel Zenon sans prelude	filliatr	2006-03-27
*	utilisation de la VM pour la normalisation finale de romega	letouzey	2006-03-24
*	correctifs de bug pour romega:	letouzey	2006-03-23
*	Subtac fixes, single fixpoint definitions are working again. Added a toggle o...	msozeau	2006-03-22
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	Adding "New Functional Scheme"	jforest	2006-03-20
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Cleaning dead code	jforest	2006-03-16
*	+ Debugging and cleaning functional principle generation tactic	jforest	2006-03-14
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
*	cleaning	jforest	2006-03-10
*	Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...	jforest	2006-03-07
*	Exploitation du 'let rec' + présentation	herbelin	2006-03-05
*	New files for subtac	coq	2006-03-05
*	tactic haRVey pour appeler haRVey (contrib/dp)	filliatr	2006-03-02
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
*	appel de Zenon	filliatr	2006-03-01
*	* empty log message *	filliatr	2006-02-28
*	dp: sortie Why	filliatr	2006-02-27
*	Work on recursive definitions	coq	2006-02-22
*	Add vernacular file for subtac	coq	2006-02-22
*	Julien:	bertot	2006-02-22
*	Work with binder lists, problem of tycons	coq	2006-02-21
*	Latest fixes, should work fine now for non recursive definitions, although st...	coq	2006-02-21
*	Fix minor bug	coq	2006-02-20