(* If you wish to step thorugh the proof files of this example in your
   Coq IDE, you should include this file so that the IDE can find
   the compiled MSL libraries.
 *)

Add LoadPath "../../..".