coq - The formal proof system

Age	Commit message (Expand)	Author
2008-04-17	Prevent the apparition of &&& when printing a (if ... then ... else false)	letouzey
2008-04-03	Rework of FMapAVL inspired by recent changes of FSetAVL:	letouzey
2008-03-27	- notations &&& and \|\|\| equivalent to andb and orb,	letouzey
2008-03-21	One more AVL reorganisation: separate pure functions from proofs + functional...	letouzey
2008-03-21	Some "if then else" instead of orb and andb, in order to vm_compute lazily	letouzey
2008-03-20	still some useless invariants in FSetAVL	letouzey
2008-03-19	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey
2008-03-15	Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)	letouzey
2008-03-07	repair FSets/FMap after the change in setoid rewrite	letouzey
2008-03-04	migration from Set to Type of FSet/FMap + some dependencies...	letouzey
2008-02-28	Nicer third spec of choose.	letouzey
2008-02-27	For more uniformity, use implicits in FSetAVL	letouzey
2008-02-09	Major revision of FSetAVL: more Function, including some non-structural ones	letouzey
2008-02-05	kill some useless module aliases E:=X (for better name printing, see Elie's 1...	letouzey
2007-10-29	Revision of the FSetWeak Interface, so that it becomes a precise	letouzey
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-13	Deletion of some firstorder calls in FSetAVL:	letouzey
2007-06-07	* For uniformity, FSetAVL uses Implicit Arguments (a bit)	letouzey
2007-05-27	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey
2007-05-25	fix for bug #1347 (no more Scope pollution by FSets)	letouzey
2007-02-28	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey
2006-06-23	Passage des graphes de Function dans Type	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-24	Suite changement précédence by de assert	herbelin
2006-05-22	suite des marquages de types et opacifications de lemmes dans les wrappers Make	letouzey
2006-05-20	suite tentative pour permettre l'utilisation de modules de FSets	letouzey
2006-04-29	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey
2003-06-24	suppression de FSets (redevient une contrib)	filliatr
2003-06-24	doc	filliatr
2003-06-24	concat; debut split	filliatr
2003-06-23	join	filliatr
2003-06-23	add_tree : sur type tree plutot que sur type t	filliatr
2003-06-23	merge_bis et debug join	filliatr
2003-06-20	remov	filliatr
2003-06-20	merge	filliatr
2003-06-20	remove_min, remove_max	filliatr
2003-06-19	add	filliatr
2003-06-19	bal: preuve terminee	filliatr
2003-06-19	bal: premier cas hl > hr + 2	filliatr
2003-06-19	typo	filliatr
2003-06-18	AVL: suite	filliatr
2003-06-17	AVL: suite	filliatr
2003-06-17	AVL de caml: un debut	filliatr