1 files changed, 0 insertions, 60 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
deleted file mode 100644
index 601cabe0..00000000
--- a/contrib/setoid_ring/ArithRing.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Mult.
-Require Import BinNat.
-Require Import Nnat.
-Require Export Ring.
-Set Implicit Arguments.
-
-Lemma natSRth : semi_ring_theory O (S O) plus mult (@eq nat).
- Proof.
-  constructor. exact plus_0_l. exact plus_comm. exact plus_assoc.
-  exact mult_1_l. exact mult_0_l. exact mult_comm. exact mult_assoc.
-  exact mult_plus_distr_r. 
- Qed.
-
-Lemma nat_morph_N : 
-   semi_morph 0 1 plus mult (eq (A:=nat)) 
-          0%N 1%N Nplus Nmult Neq_bool nat_of_N.
-Proof.
-  constructor;trivial.
-  exact nat_of_Nplus.
-  exact nat_of_Nmult.
-  intros x y H;rewrite (Neq_bool_ok _ _ H);trivial.
-Qed.
-
-Ltac natcst t :=
-  match isnatcst t with
-    true => constr:(N_of_nat t)
-  | _ => constr:InitialRing.NotConstant
-  end.
-
-Ltac Ss_to_add f acc :=
-  match f with
-  | S ?f1 => Ss_to_add f1 (S acc)
-  | _ => constr:(acc + f)%nat
-  end.
-
-Ltac natprering :=
-  match goal with
-    |- context C [S ?p] =>
-    match p with
-      O => fail 1 (* avoid replacing 1 with 1+0 ! *)
-    | p => match isnatcst p with 
-           | true => fail 1
-           | false => let v := Ss_to_add p (S 0) in
-                         fold v; natprering
-           end
-    end
-  | _ => idtac
-  end.
-
-Add Ring natr : natSRth
-  (morphism nat_morph_N, constants [natcst], preprocess [natprering]).
-