coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction bug #1192	notin	2006-07-18
*	Code cleaning in Function	jforest	2006-07-18
*	Code cleaning in Function	jforest	2006-07-18
*	bug correction when defining graph of fixpoints/definitions not generated by ...	jforest	2006-07-13
*	Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...	herbelin	2006-07-11
*	+functional inversion now takes the function to invert as an optional argument.	jforest	2006-07-10
*	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin	2006-07-07
*	Suite remplacement VernacDebug par VernacSetOption	herbelin	2006-07-06
*	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
*	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