Remove the broken test cases

math-comp · May 28, 2024 · 0132827 · 0132827
1 parent 610d3d0
commit 0132827
Showing 1 changed file with 0 additions and 10 deletions.
diff --git a/examples/test_ssreflect.v b/examples/test_ssreflect.v
@@ -106,27 +106,17 @@ Proof. zify_op; reflexivity. Qed.
 Fact test_eq_op_nat n m : (n == m) = Z.eqb (Z.of_nat n) (Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_addn_rec n m : Z.of_nat (n + m)%Nrec = (Z.of_nat n + Z.of_nat m)%Z.
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_addn n m : Z.of_nat (n + m) = (Z.of_nat n + Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.
 
 Fact test_addn_trec n m :
   Z.of_nat (NatTrec.add n m) = (Z.of_nat n + Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_subn_rec n m :
-  Z.of_nat (n - m)%Nrec = Z.max 0 (Z.of_nat n - Z.of_nat m).
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_subn n m :
   Z.of_nat (n - m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_muln_rec n m : Z.of_nat (n * m)%Nrec = (Z.of_nat n * Z.of_nat m)%Z.
-Proof. zify_op; reflexivity. Qed.
-
 Fact test_muln n m : Z.of_nat (n * m) = (Z.of_nat n * Z.of_nat m)%Z.
 Proof. zify_op; reflexivity. Qed.