Commit 9739d4ab authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Fix sessions that wrongly recorded a failed proof attempt by Coq.Interval

parent efc4acd8
......@@ -9,7 +9,7 @@
<file name="../my_cosine.why" expanded="true">
<theory name="CosineSingle" sum="755ee8878730ca0c5dd106b03f1b8590" expanded="true">
<goal name="MethodError" expanded="true">
<proof prover="0" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="unknown" time="1.44"/></proof>
<proof prover="0" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="3.65"/></proof>
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="TotalErrorFullyExpanded" expanded="true">
......
......@@ -9,7 +9,7 @@
<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="0" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="unknown" time="1.37"/></proof>
<proof prover="0" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="3.46"/></proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="2. precondition" expanded="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
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