aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-17 15:07:59 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-17 15:07:59 +0200
commit0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (patch)
treee449e76c73088a6cae457d1210f836581093807a /tactics
parenteba5d64fee0bf6235265f1f6cc884b4cbefe2704 (diff)
parenta2bc4d3be684ad24ea7888df4dd0cf35d9733c64 (diff)
Merge PR #781: Remove dead code [Universes.simplify_universe_context]
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions