coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Add enough information to correctly globalize recursive calls in inductive and	msozeau	2008-09-11
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Postpone the search for the recursive argument index from the user given	msozeau	2008-05-06
*	correction of bug 1829	jforest	2008-04-08
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Adapt funind to the RLetPattern constructor.	msozeau	2008-03-15
*	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau	2008-01-17
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest	2007-03-16
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Retour r9310 en attendant mieux	herbelin	2007-02-09
*	Meilleur anglais (cf 9619)	herbelin	2007-02-07
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Detection des paramettres pour les Functions bien fondees	jforest	2006-09-27
*	Gestion des arguments implicites dans les Functions bien fondees	jforest	2006-09-19
*	correction of bug #1220	jforest	2006-09-18
*	mise en conformite des messages d'erreur de Function avec la doc.	jforest	2006-09-14
*	Amelioration des messages d'erreur de Fucntion	jforest	2006-08-24
*	Bug corrections in Function.	jforest	2006-08-11
*	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
*	+functional inversion now takes the function to invert as an optional argument.	jforest	2006-07-10
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	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
*	LetTuple are now supported in Function	jforest	2006-05-22
*	Correction in generate_graph (now handles fun _ => fix ....)	jforest	2006-05-05
*	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest	2006-05-03
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Adding "New Functional Scheme"	jforest	2006-03-20
*	+ Debugging and cleaning functional principle generation tactic	jforest	2006-03-14
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Julien:	bertot	2006-02-22
*	Julien:	bertot	2006-02-17
*	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot	2006-02-08
*	Julien:	bertot	2006-02-08