coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...	barras	2006-09-28
*	Add dependent list combinators test.	msozeau	2006-09-28
*	Detection des paramettres pour les Functions bien fondees	jforest	2006-09-27
*	petits pbs de dependances	barras	2006-09-26
*	Compilation newring	notin	2006-09-26
*	commit de field + renommages	barras	2006-09-26
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Gestion des arguments implicites dans les Functions bien fondees	jforest	2006-09-19
*	added congruence improvement	corbinea	2006-09-19
*	correction of bug #1220	jforest	2006-09-18
*	Message modification in Function	jforest	2006-09-16
*	Minor bug correction in well-founded Function.	jforest	2006-09-15
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	mise en conformite des messages d'erreur de Function avec la doc.	jforest	2006-09-14
*	Fix wrong order for building library, add informative messages.	msozeau	2006-09-04
*	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-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