Update documentation of the Why3 API
Hello,
I use the Why3 directly in OCaml. In particular I use the Ptree
module. Unfortunately the documentation is very succinct.
For example, I cannot understand what the Eoptexn
constructor does. Is it the declaration of a local exception? Is this local exception caught at the end of the block?
It would be a great improvement if all constructors have their own documentation and it would significantly help the Why3 users.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information