coq - The formal proof system

Age	Commit message (Expand)	Author
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-03-16	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest
2006-11-23	Fixing syntax and parameter order in functional graph merging.	courtieu
2006-11-20	Changing merging functional scheme syntax.	courtieu
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-20	Starting to add a function schemes merging command (not finished, not	courtieu
2006-09-18	correction of bug #1220	jforest
2006-08-15	working on functional induction automation (tactic finduction and	courtieu
2006-07-10	+functional inversion now takes the function to invert as an optional argument.	jforest
2006-07-04	functional inversion now takes a quatified hypothesis as first argument	jforest
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
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-07	functional induction can now be used with	jforest
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-05-31	Replacing the old version of "functional induction" with the new one.	jforest
2006-05-29	small changes	jforest
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-04-26	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest
2006-04-10	+ Changing a little functional schemes types	jforest
2006-03-20	Adding "New Functional Scheme"	jforest
2006-03-16	Cleaning dead code	jforest
2006-03-14	+ Debugging and cleaning functional principle generation tactic	jforest
2006-03-12	-Debugging multiple induction, a bug appeared when having function	courtieu
2006-02-22	Julien:	bertot
2006-02-17	Julien:	bertot
2006-02-08	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot
2006-02-08	Julien:	bertot
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq