aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-02 11:00:04 +0000
committerGitHub2020-12-02 11:00:04 +0000
commitff8155bf6586040b92d916a72017ac1bdc138501 (patch)
tree69744806c326313960ecb53c53d56ae7bf299928 /tactics
parentb3b4d641dafe58ad04932c5bb5cc2f4f3f54d91f (diff)
parent64de97e5f16d3c52f73fb126ca64c85382c2a3d4 (diff)
Merge PR #13543: Fix a bug in funind.
Reviewed-by: Matafou
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions