coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	adding comments and cleaning code	jforest	2006-07-04
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin	2006-07-03
*	forgot a file	jforest	2006-06-29
*	bug correction	jforest	2006-06-29
*	Passage des graphes de Function dans Type	jforest	2006-06-23
*	Fix wrong order of existentials in eterm.	msozeau	2006-06-23
*	Suite passage ident -> hyp dans syntaxe de 'replace with in'	herbelin	2006-06-23
*	Mutually structurally recursive defs and rec using measures added.	msozeau	2006-06-22
*	Wellfounded recursion using subtac working again.	msozeau	2006-06-20
*	Progress in new wf def typing.	msozeau	2006-06-20
*	Rewrite of the recursive defs handling in progress.	msozeau	2006-06-20
*	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
*	Bug suite déplacement Int.v dans ZArith	herbelin	2006-06-09
*	oups: il faut penser a fermer la porte en partant (d'un fixpoint)	letouzey	2006-06-09
*	changements de dernieres minutes pour la 8.1 beta:	letouzey	2006-06-09
*	Changement du type d'argument 'TacticArgType X' en un type	herbelin	2006-06-08
*	reparation bug 1006	letouzey	2006-06-08
*	DÃ©tection bug rawwit suitecorrection trou de typage create_arg	herbelin	2006-06-08
*	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin	2006-06-07
*	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
*	debut de reparation du test d'extraction	letouzey	2006-06-02
*	Fix some nasty bug with the evars-to-dependent sum encoding.	msozeau	2006-06-01
*	bug in alpha-conversion	jforest	2006-06-01
*	reparation bug #1128	letouzey	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
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	small changes	jforest	2006-05-29
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	removing a warning	jforest	2006-05-26
*	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
*	Clarification role de library_part : renommage en remove_section_part	herbelin	2006-05-23
*	cleanning code	jforest	2006-05-23
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Correcting a bug in identifiers manipulation	jforest	2006-05-22
*	LetTuple are now supported in Function	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
*	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