coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07
*	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau	2007-07-19
*	Better handling of aliases, add command to solve a particular obligation.	msozeau	2007-07-02
*	Add Solve All Obligations command, fix bug in inequality generation introduce...	msozeau	2007-06-14
*	Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...	msozeau	2007-06-09
*	Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...	msozeau	2007-03-20
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Add destruct_call variant where naming of introduced hypotheses is possible. ...	msozeau	2007-03-15
*	Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...	msozeau	2007-03-14
*	Opacity parameterization for obligations working.	msozeau	2007-02-24
*	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau	2007-02-19
*	Various little subtac fixes, add some useful tactics.	msozeau	2007-02-19
*	Separate Tactics in subtac.	msozeau	2007-02-09
*	Fix mistake naming my Tactics file Tactics :)	msozeau	2007-02-07