coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use typing informations while defining graphs for Function.	jforest	2006-07-05
*	functional inversion now takes a quatified hypothesis as first argument	jforest	2006-07-04
*	adding comments and cleaning code	jforest	2006-07-04
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	forgot a file	jforest	2006-06-29
*	bug correction	jforest	2006-06-29
*	Passage des graphes de Function dans Type	jforest	2006-06-23
*	Ajout de tactiques expérimentales basée sur functional induction.	courtieu	2006-06-16
*	ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...	jforest	2006-06-13
*	rearrangement du code: deplacement du code effectuant functional	courtieu	2006-06-13
*	changed comments.	courtieu	2006-06-12
*	functional induction can now be used with	jforest	2006-06-07
*	this time it's good	jforest	2006-06-06
*	Error in last commit	jforest	2006-06-06
*	protecting an uncaught exception Not_found	jforest	2006-06-06
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	bug in alpha-conversion	jforest	2006-06-01
*	Replacing the old version of "functional induction" with the new one.	jforest	2006-05-31
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	small changes	jforest	2006-05-29
*	Error during last commit (coq didn't compile)	jforest	2006-05-23
*	Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)	jforest	2006-05-23
*	LetTuple are now supported in Function	jforest	2006-05-22
*	+ 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
*	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
*	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
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	Simplifying the proof of principles	jforest	2006-04-12
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Adding "New Functional Scheme"	jforest	2006-03-20
*	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
*	Julien:	bertot	2006-02-22
*	Julien:	bertot	2006-02-17
*	changed the decomposition of an induction scheme	coq	2006-02-17
*	very minor bug correction and cleanning	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
*	added mli 's for the nex functional induction (forgotten last time).	coq	2006-02-03
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01