diff options
author | Armaël Guéneau <armael.gueneau@ens-lyon.fr> | 2018-05-31 12:02:09 +0200 |
---|---|---|
committer | Armaël Guéneau <armael.gueneau@ens-lyon.fr> | 2018-05-31 14:26:52 +0200 |
commit | aec09817bfa5951d6b99e670ee04bf8dbc20c209 (patch) | |
tree | bf4fc7ce5050ed677121af9ae573d3d44ce35f09 /interp/modintern.ml | |
parent | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff) |
Remove some dead code in class_tactics.ml
Diffstat (limited to 'interp/modintern.ml')
0 files changed, 0 insertions, 0 deletions