coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Debug wellfounded defs, work on cleaning obls envs	msozeau	2007-02-23
*	Various little subtac fixes, add some useful tactics.	msozeau	2007-02-19
*	Various subtac fixes.	msozeau	2007-01-15
*	Support for mutual defs in obligation handling.	msozeau	2006-11-09
*	Work on obligation separation.	msozeau	2006-10-31
*	Facilities to automatically solve obligations	msozeau	2006-10-26
*	New handling of obligations.	msozeau	2006-09-01
*	Fix some nasty bug with the evars-to-dependent sum encoding.	msozeau	2006-06-01
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	Subtac fixes, single fixpoint definitions are working again. Added a toggle o...	msozeau	2006-03-22
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22