-
Mário Pereira authored
The code in file /src/util/pqueue.ml has been extracted from a Why3 proof, and is now a correct-by-construction OCaml code. This file depends on the Vector module, which is also an OCaml implementation extracted from another Why3 proof. The proofs can be found in /examples/util/ This is the result of Aymeric Walch bachelor internship.
0da5f41e