remove the sequenceV call from bff
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 11:49:45 +0000 (12:49 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 26 Feb 2014 11:49:45 +0000 (12:49 +0100)
commitaad47e05ef1567285aca67b3c8030e36929703b4
treec5fc45821f2a7c0277eccb385dfda0f786c84de5
parentbec4b138090e87fe92c970ca98010e60707c44f9
remove the sequenceV call from bff

This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.
BFF.agda
BFFPlug.agda
Bidir.agda
Precond.agda