Commit 25554264 authored by MARCHE Claude's avatar MARCHE Claude

small fix on session

parent 26a47423
......@@ -3,14 +3,14 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="2" memlimit="0"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="8" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" memlimit="1000"/>
<file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="824a378ddc65f51c5ce6a6ff77de21e0" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="1" edited="my_cosine_M_WP_parameter_my_cosine_1.v" obsolete="true"><undone/></proof>
<proof prover="1" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="4.07"/></proof>
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. precondition" expanded="true">
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment