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
*	- 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
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Functional graph merging deals with letins.	courtieu	2006-11-24
*	Experimental merging of two functional graphs.	courtieu	2006-10-26
*	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest	2006-08-16
*	+functional inversion now takes the function to invert as an optional argument.	jforest	2006-07-10
*	Use typing informations while defining graphs for Function.	jforest	2006-07-05
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	bug in alpha-conversion	jforest	2006-06-01
*	LetTuple are now supported in Function	jforest	2006-05-22
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...	jforest	2006-03-07
*	Julien:	bertot	2006-02-17
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01