aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/eterm.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-25Partial fix for bug #1948: recompute order of dependencies betweenmsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-08-21Various fixes w.r.t typeclasses and subtac: resolve tcs properly insidemsozeau
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
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-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-02-24Opacity parameterization for obligations working.msozeau
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
2006-10-31Work on obligation separation.msozeau
2006-09-01New handling of obligations.msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2005-07-15Subtac: traitement correct des existentielles et de la récursion.coq