coq - The formal proof system

Age	Commit message (Expand)	Author
2007-04-17	Correct implementation of undo in obligations handling code, correct some bug...	msozeau
2007-03-28	Support for implicit formal argument types in Program ; parse types in type s...	msozeau
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-27	Fix wf bug from F. Besson and work on ineqs generation.	msozeau
2007-02-23	Debug wellfounded defs, work on cleaning obls envs	msozeau
2007-02-19	Various little subtac fixes, add some useful tactics.	msozeau
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-07	Various subtac fixes. Add inequalities in pattern matching branches when need...	msozeau
2007-01-15	Various subtac fixes.	msozeau
2006-12-08	Subtac bug fix, add list take example.	msozeau
2006-11-10	Work on mutual defs, various bug fixes.	msozeau
2006-11-10	Work on pattern inequalities for pattern matching branches.	msozeau
2006-11-09	Support for mutual defs in obligation handling.	msozeau
2006-10-31	Work on obligation separation.	msozeau
2006-10-26	Facilities to automatically solve obligations	msozeau
2006-10-10	Fix 0 obligations bug	msozeau
2006-09-01	New handling of obligations.	msozeau
2006-09-01	Subtac fixes, new way of handling obligations in progress.	msozeau
2006-06-22	Mutually structurally recursive defs and rec using measures added.	msozeau
2006-06-20	Wellfounded recursion using subtac working again.	msozeau
2006-06-20	Progress in new wf def typing.	msozeau
2006-06-20	Rewrite of the recursive defs handling in progress.	msozeau
2006-06-01	Fix some nasty bug with the evars-to-dependent sum encoding.	msozeau
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-10	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-03-22	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-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau