aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_obligations.mli
AgeCommit message (Expand)Author
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-02Noise for nothingpboutill
2011-06-30Keep obligation source information in Programmsozeau
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
2010-01-26Add [Next Obligation with tactic] support (wish #1953).msozeau
2010-01-14- Show Obligation Tacticmsozeau
2010-01-11Support "Local Obligation Tactic" (now the default in sections).msozeau
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-05-16Support for definition hooks in subtac.msozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey