mirror of
https://github.com/AdaCore/SPARKlib.git
synced 2026-02-12 13:11:36 -08:00
* 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