aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-12-07 14:07:28 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-03 20:05:57 +0200
commit173f32406be06ad4dfcecf3cda6070543d68d715 (patch)
tree078d4520007921fa0fc2a69516b8996ab88f21b7 /library
parent3b57395029447119eea1fd399636cd9cfe3e673e (diff)
Generalizing the tactic-in-term embedding to any generic argument.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions