* generate_session.py
- show proved VC when running Coq; this helps detect when the
--limit-line argument is incorrect
- delete more files
- remove useless level argument to call of run_automatic
* manual_proof.in: fixed locations of checks
* lemma_raising_order_*.prf: fixed proof of lemma, the proof is now much
simpler
This patch copies and adapts the source files of SPARKlib from the spark2014
repository into this one. It also changes the license of these files, as
SPARKlib is now licensed under Apache 2.0.
