coq - The formal proof system

Age	Commit message (Expand)	Author
2006-09-15	Minor bug correction in well-founded Function.	jforest
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-14	mise en conformite des messages d'erreur de Function avec la doc.	jforest
2006-09-04	Fix wrong order for building library, add informative messages.	msozeau
2006-09-01	New handling of obligations.	msozeau
2006-09-01	Forgot to add this one.	msozeau
2006-09-01	Subtac fixes, new way of handling obligations in progress.	msozeau
2006-09-01	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin
2006-08-25	two minor bug corrections in General Recursive Functions	jforest
2006-08-24	Amelioration des messages d'erreur de Fucntion	jforest
2006-08-22	making otags working	jforest
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-08-16	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest
2006-08-15	working on functional induction automation (tactic finduction and	courtieu
2006-08-11	Bug corrections in Function.	jforest
2006-08-08	In the old version, recursive functions cannot be declared inside a section	bertot
2006-07-18	Correction bug #1192	notin
2006-07-18	Code cleaning in Function	jforest
2006-07-18	Code cleaning in Function	jforest
2006-07-13	bug correction when defining graph of fixpoints/definitions not generated by ...	jforest
2006-07-11	Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...	herbelin
2006-07-10	+functional inversion now takes the function to invert as an optional argument.	jforest
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-07-06	Suite remplacement VernacDebug par VernacSetOption	herbelin
2006-07-05	Use typing informations while defining graphs for Function.	jforest
2006-07-04	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-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-06-29	forgot a file	jforest
2006-06-29	bug correction	jforest
2006-06-23	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-22	Mutually structurally recursive defs and rec using measures added.	msozeau
2006-06-20	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-16	Ajout de tactiques expérimentales basée sur functional induction.	courtieu
2006-06-13	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-12	changed comments.	courtieu
2006-06-09	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-08	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-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin