aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-04 20:42:07 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-04 21:23:59 +0100
commit0aba678e885fa53fa649de59eb1d06b4af3a847c (patch)
tree127cd9e0e3600b17cf6b40e762e671ec9bf4628a /library
parent86304bddaff73bdc0f8aa6c7619d806c001040ec (diff)
Getting rid of the dynamic node of the tactic AST.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions