aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/btermdn.mli
diff options
context:
space:
mode:
authorGravatar Armaël Guéneau <armael.gueneau@ens-lyon.fr>2018-05-29 11:29:39 +0200
committerGravatar Armaël Guéneau <armael.gueneau@ens-lyon.fr>2018-05-29 11:29:39 +0200
commit70187829867cfc19ec6ee5372e3c5f020fbf604e (patch)
treed328e08142bacdad034cfa1dbb1f704a75a7231c /tactics/btermdn.mli
parent81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff)
Fix anomaly in autoapply when an unbound hint name is provided
Diffstat (limited to 'tactics/btermdn.mli')
0 files changed, 0 insertions, 0 deletions