aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/btermdn.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2015-10-05 17:00:11 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2015-10-05 17:24:50 +0200
commit92ee78086f1ca89646ac69a00256ff45fcaee22c (patch)
tree331667abdc4598f1b04e5b6ca0e758bff65a2f39 /tactics/btermdn.mli
parentbba2cfb5921653f18d6cedf2800cdc1abf9310af (diff)
Univs: fix printing bug #3797.
Diffstat (limited to 'tactics/btermdn.mli')
0 files changed, 0 insertions, 0 deletions