coq - The formal proof system

Age	Commit message (Expand)	Author
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