aboutsummaryrefslogtreecommitdiff
path: root/src/tac2expr.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-10-01 19:10:11 +0200
committerPierre-Marie Pédrot2017-10-01 19:18:59 +0200
commit0145084daa86b35a1d2a8285c4e16a9a231e3652 (patch)
tree5a589caf12c346ec9a1ac17521d35a07191eddd5 /src/tac2expr.mli
parent95f0ba81363a464e416fa2fdba3e4170accd4d96 (diff)
Using Ltac2 native closures in some tactic APIs.
Diffstat (limited to 'src/tac2expr.mli')
0 files changed, 0 insertions, 0 deletions