aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-08-18 00:02:45 +0200
committerPierre-Marie Pédrot2014-08-18 01:15:43 +0200
commit243ffa4b928486122075762da6ce8da707e07daf (patch)
tree3870e1b1d3059ba13158a73df7c5f3b300e504ce /dev/doc
parent6dd9e003c289a79b0656e7c6f2cc59935997370c (diff)
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions