coq - The formal proof system

Age	Commit message (Expand)	Author
2012-05-25	Bugs revealed by playing with contribs	pboutill
2012-05-11	Vectors takes advantage of pattern matching compiler fixup	pboutill
2012-05-02	Coqide highligthing is back (done by gtksourceview).	pboutill
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-02-29	Vector: missing injection lemmas and better impossible branches	pboutill
2011-12-07	Vectors use a bit more the pattern matching compiler	pboutill
2011-11-21	VectorDef.v takes benefit of dependencies being taken into account	herbelin
2011-08-10	Less ambitious application of a notation for eq_rect. We proposed	herbelin
2011-08-08	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin
2011-07-16	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin
2011-05-03	As many notation for for vectors as for List.	pboutill
2011-03-23	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau
2011-03-11	Inference of match predicate produces ill-typed unification problem,	msozeau
2011-02-10	Vectors fully use implicit arguments	pboutill
2011-02-10	Fixpoints are traverse during implicits arguments search to toplevel	pboutill
2011-02-10	Interp a definition with the implicit arguments of its local context	pboutill
2011-02-10	local variables can have implicits locally	pboutill
2011-02-10	Data structure telling implicits of local variables is a map in the	pboutill
2010-12-10	First release of Vector library.	pboutill