aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-06 09:47:47 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-06 09:47:47 +0100
commit9122b9244ed0907ce91b50bbe3584d69cb340baa (patch)
tree2cdfa907b1e1fb08f48520aa7682d21e6372e539 /checker
parent7b14d01ccc41b47df9644391bf01e4b7949e571d (diff)
parentb80f10a95692c3e4fd95f5ed196311e22fc044b4 (diff)
Merge PR #6900: [compat] Remove "Tactic Pattern Unification"
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions