fixed proofs on moloch

examples/bitvectors/double/why3session.xml

@@ -20,7 +20,7 @@
  <prover
   id="4"
   name="Coq"
-  version="8.4"/>
+  version="8.3pl4"/>
  <prover
   id="5"
   name="Z3"
@@ -185,7 +185,7 @@
      edited="double_TestDouble_exp_one_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.19"/>
+     <result status="valid" time="0.61"/>
     </proof>
    </goal>
    <goal

examples/bitvectors/double_of_int/why3session.xml

@@ -20,11 +20,11 @@
  <prover
   id="4"
   name="Coq"
-  version="8.4"/>
+  version="8.3pl4"/>
  <prover
   id="5"
   name="Gappa"
-  version="0.16.0"/>
+  version="0.16.1"/>
  <prover
   id="6"
   name="Z3"
@@ -65,7 +65,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.42"/>
+     <result status="valid" time="1.06"/>
     </proof>
    </goal>
    <goal
@@ -90,7 +90,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.75"/>
+     <result status="valid" time="0.57"/>
     </proof>
    </goal>
    <goal
@@ -107,7 +107,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.35"/>
+     <result status="valid" time="1.86"/>
     </proof>
     <proof
      prover="1"
@@ -115,7 +115,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.45"/>
+     <result status="valid" time="1.08"/>
     </proof>
    </goal>
    <goal
@@ -140,7 +140,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.76"/>
+     <result status="valid" time="0.55"/>
     </proof>
    </goal>
    <goal
@@ -540,7 +540,7 @@
      edited="double_of_int_DoubleOfInt_exp_const_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.68"/>
+     <result status="valid" time="0.95"/>
     </proof>
    </goal>
    <goal
@@ -597,7 +597,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.71"/>
+     <result status="valid" time="3.21"/>
     </proof>
    </goal>
    <goal
@@ -867,7 +867,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="13.17"/>
+     <result status="valid" time="11.70"/>
     </proof>
     <proof
      prover="1"
@@ -1180,7 +1180,7 @@
      edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.34"/>
+     <result status="valid" time="2.54"/>
     </proof>
    </goal>
    <goal
@@ -1198,7 +1198,7 @@
      edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="9.64"/>
+     <result status="valid" time="8.10"/>
     </proof>
    </goal>
    <goal
@@ -1257,7 +1257,7 @@
      edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="4.09"/>
+     <result status="valid" time="3.07"/>
     </proof>
    </goal>
    <goal
@@ -1275,7 +1275,7 @@
      edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.43"/>
+     <result status="valid" time="0.69"/>
     </proof>
    </goal>
    <goal
@@ -1375,7 +1375,7 @@
      edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.36"/>
+     <result status="valid" time="2.37"/>
     </proof>
    </goal>
    <goal
@@ -1700,7 +1700,7 @@
      edited="double_of_int_DoubleOfInt_lemma3_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="4.03"/>
+     <result status="valid" time="3.31"/>
     </proof>
    </goal>
    <goal
@@ -1889,7 +1889,7 @@
      edited="double_of_int_DoubleOfInt_var_value0_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.47"/>
+     <result status="valid" time="1.88"/>
     </proof>
    </goal>
    <goal

examples/bitvectors/neg_as_xor/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Coq"
-  version="8.4"/>
+  version="8.3pl4"/>
  <prover
   id="3"
   name="Z3"
@@ -327,7 +327,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.97"/>
+     <result status="valid" time="1.21"/>
     </proof>
     <proof
      prover="4"
@@ -370,7 +370,7 @@
      edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.70"/>
+     <result status="valid" time="1.17"/>
     </proof>
    </goal>
   </theory>

examples/bitvectors/power2/why3session.xml

@@ -24,11 +24,11 @@
  <prover
   id="5"
   name="Coq"
-  version="8.4"/>
+  version="8.3pl4"/>
  <prover
   id="6"
   name="Gappa"
-  version="0.16.0"/>
+  version="0.16.1"/>
  <prover
   id="7"
   name="Z3"
@@ -111,7 +111,7 @@
      edited="power2_Pow2int_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.26"/>
+     <result status="valid" time="0.77"/>
     </proof>
    </goal>
    <goal
@@ -129,7 +129,7 @@
      edited="power2_Pow2int_pow2pos_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.11"/>
+     <result status="valid" time="0.59"/>
     </proof>
    </goal>
    <goal
@@ -3351,7 +3351,7 @@
      edited="power2_Pow2int_Mod_pow2_gen_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.66"/>
+     <result status="valid" time="1.20"/>
     </proof>
    </goal>
   </theory>
@@ -3629,7 +3629,7 @@
      edited="power2_Pow2real_Power_non_null_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.22"/>
+     <result status="valid" time="0.58"/>
     </proof>
    </goal>
    <goal
@@ -3647,7 +3647,7 @@
      edited="power2_Pow2real_Power_neg_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.34"/>
+     <result status="valid" time="0.74"/>
     </proof>
    </goal>
    <goal
@@ -3665,7 +3665,7 @@
      edited="power2_Pow2real_Power_non_null_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.28"/>
+     <result status="valid" time="0.67"/>
     </proof>
    </goal>
    <goal
@@ -3708,7 +3708,7 @@
      edited="power2_Pow2real_Power_sum_aux_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.30"/>
+     <result status="valid" time="0.72"/>
     </proof>
    </goal>
    <goal
@@ -3726,7 +3726,7 @@
      edited="power2_Pow2real_Power_sum_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.37"/>
+     <result status="valid" time="0.83"/>
     </proof>
    </goal>
    <goal
@@ -3744,7 +3744,7 @@
      edited="power2_Pow2real_Pow2_int_real_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.19"/>
+     <result status="valid" time="0.59"/>
     </proof>
    </goal>
   </theory>

lib/coq/int/EuclideanDivision.v

@@ -166,7 +166,6 @@ unfold mod1.
 rewrite Div_minus1_left; auto with zarith.
 Qed.
 
-Require ZArith.Zquot.
 Open Scope Z_scope.
 
 (* Why3 goal *)