aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-12 09:58:59 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-12 09:58:59 +0100
commit349944eb8e3abd51dc2b94051a887253a2ae9198 (patch)
treefc6eb1aac341a3258d3ddc4d2c660aed67bed190 /plugins/funind
parent47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff)
parent1da06b3c3dafaff0d71f36ecf2c732fd90429a86 (diff)
Merge PR #6674: Delay computation of lifts in the reduction machine.
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions