aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_obligations.mli
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-11-07Add the ability to give a specific tactic to solve each obligation inmsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-10-24Fix some bugs, add possibility of automatically solving a proof statement's o...msozeau
2007-07-12Fix bug when adding progs with no obligationsmsozeau
2007-07-02Better handling of aliases, add command to solve a particular obligation.msozeau
2007-06-14Add Solve All Obligations command, fix bug in inequality generation introduce...msozeau
2007-04-17Correct implementation of undo in obligations handling code, correct some bug...msozeau
2007-03-13Solve obligation handling bug of trying to solve automatically at Next Obliga...msozeau
2007-02-24Opacity parameterization for obligations working.msozeau
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when need...msozeau
2007-01-15Various subtac fixes.msozeau
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-11-15Some usability enhancements.msozeau
2006-11-10Work on mutual defs, various bug fixes.msozeau
2006-11-09Support for mutual defs in obligation handling.msozeau
2006-10-31Work on obligation separation.msozeau
2006-10-26Facilities to automatically solve obligationsmsozeau