From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 contrib7/ring/Ring.v | 34 ----------------------------------
 1 file changed, 34 deletions(-)
 delete mode 100644 contrib7/ring/Ring.v

(limited to 'contrib7/ring/Ring.v')

diff --git a/contrib7/ring/Ring.v b/contrib7/ring/Ring.v
deleted file mode 100644
index 860dda13..00000000
--- a/contrib7/ring/Ring.v
+++ /dev/null
@@ -1,34 +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: Ring.v,v 1.1.2.1 2004/07/16 19:30:18 herbelin Exp $ *)
-
-Require Export Bool.
-Require Export Ring_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 [b:bool]b eqb).
-Split; Simpl.
-NewDestruct n; NewDestruct m; Reflexivity.
-NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
-NewDestruct n; NewDestruct m; Reflexivity.
-NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
-NewDestruct n; Reflexivity.
-NewDestruct n; Reflexivity.
-NewDestruct n; Reflexivity.
-NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
-NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto.
-Defined.
-
-Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ].
-- 
cgit v1.2.3