A Datastructure for Iterated Powers

• the Coq vernacular file BshnFinal.v with the implementation
• the documentation generated from coqdoc
• the index of all Coq elements in BshnFinal.v

There is also a version BshnFinal81.v for use with Coq V8.1 pl2 (October 23, 2007).

Now also a version BshnFinal84.v tested with Coq V8.4 pl1 (December 28, 2012). It uses the library Vector instead of Bvector.