1 files changed, 0 insertions, 36 deletions
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
deleted file mode 100644
index 40323b3d..00000000
--- a/contrib/ring/LegacyRing.v
+++ /dev/null
@@ -1,36 +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        *)
-(************************************************************************)
-
-(* $Id: LegacyRing.v 10739 2008-04-01 14:45:20Z herbelin $ *)
-
-Require Export Bool.
-Require Export LegacyRing_theory.
-Require Export Quote.
-Require Export Ring_normalize.
-Require Export Ring_abstract.
-
-(* As an example, we provide an instantation for bool. *)
-(* Other instatiations are given in ArithRing and ZArithRing in the
-   same directory *)
-
-Definition BoolTheory :
-  Ring_Theory xorb andb true false (fun b:bool => b) eqb.
-split; simpl in |- *.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct x; destruct y; reflexivity || simpl in |- *; tauto.
-Defined.
-
-Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ].