fix missing import of "length"
authorHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 07:54:51 +0000 (08:54 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sun, 25 Nov 2018 07:54:51 +0000 (08:54 +0100)
commit04e312472d4737815cf6c37258b547673faa0b91
tree101eb3d51b6cbd8a9a5309364e4b978798ea90be
parentc98062b949a6fc792b042e04453b0bed27941caa
fix missing import of "length"

Broken in parent commit.
Generic.agda