nightly bench: policy upgrade Coq8.4pl2 to pl4

examples/nightly-bench.sh

@@ -91,6 +91,15 @@ target_name = "Coq"
 target_version = "8.4pl4"
 version = "8.4pl5"
 
+[uninstalled_prover policy2]
+alternative = ""
+name = "Coq"
+policy = "upgrade"
+target_alternative = ""
+target_name = "Coq"
+target_version = "8.4pl4"
+version = "8.4pl2"
+
 EOF
 
 # run the bench

examples/random_access_list/why3session.xml

@@ -21,10 +21,10 @@
  </transf>
  </goal>
  <goal name="WP_parameter size" expl="VC for size">
- <proof prover="0"><result status="valid" time="0.02" steps="69"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
  </goal>
  <goal name="WP_parameter add" expl="VC for add">
- <proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="70"/></proof>
  </goal>
  <goal name="WP_parameter nth_flatten" expl="VC for nth_flatten">
  <transf name="split_goal_wp">
@@ -41,7 +41,7 @@
   <proof prover="6"><result status="valid" time="0.24"/></proof>
   </goal>
   <goal name="WP_parameter nth_flatten.5" expl="5. postcondition">
-  <proof prover="0" obsolete="true"><result status="unknown" time="0.04"/></proof>
+  <proof prover="0"><result status="unknown" time="0.04"/></proof>
   <proof prover="1"><result status="valid" time="0.07"/></proof>
   </goal>
  </transf>