coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin	2006-09-01
*	Ajout possibilité clause "where" dans co-points fixes	herbelin	2006-09-01
*	two minor bug corrections in General Recursive Functions	jforest	2006-08-25
*	Amelioration des messages d'erreur de Fucntion	jforest	2006-08-24
*	making otags working	jforest	2006-08-22
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest	2006-08-16
*	working on functional induction automation (tactic finduction and	courtieu	2006-08-15
*	Bug corrections in Function.	jforest	2006-08-11
*	In the old version, recursive functions cannot be declared inside a section	bertot	2006-08-08
*	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