From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 contrib/field/Field_Compl.v | 39 ++++++++-------------------------------
 1 file changed, 8 insertions(+), 31 deletions(-)

(limited to 'contrib/field/Field_Compl.v')

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index 774b3084..f018359e 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -6,56 +6,33 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field_Compl.v 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: Field_Compl.v 8866 2006-05-28 16:21:04Z herbelin $ *)
 
-Inductive listT (A:Type) : Type :=
-  | nilT : listT A
-  | consT : A -> listT A -> listT A.
-
-Fixpoint appT (A:Type) (l m:listT A) {struct l} : listT A :=
-  match l with
-  | nilT => m
-  | consT a l1 => consT A a (appT A l1 m)
-  end.
-
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
+Require Import List.
 
 Definition assoc_2nd :=
   (fix assoc_2nd_rec (A:Type) (B:Set)
                      (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
-                     (lst:listT (prodT A B)) {struct lst} : 
+                     (lst:list (prod A B)) {struct lst} : 
    B -> A -> A :=
      fun (key:B) (default:A) =>
        match lst with
-       | nilT => default
-       | consT (pairT v e) l =>
+       | nil => default
+       | (v,e) :: l =>
            match eq_dec e key with
            | left _ => v
            | right _ => assoc_2nd_rec A B eq_dec l key default
            end
        end).
 
-Definition fstT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT a _ => a
-                                            end.
-
-Definition sndT (A B:Type) (c:prodT A B) := match c with
-                                            | pairT _ a => a
-                                            end.
-
 Definition mem :=
   (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2}) 
-           (a:A) (l:listT A) {struct l} : bool :=
+           (a:A) (l:list A) {struct l} : bool :=
      match l with
-     | nilT => false
-     | consT a1 l1 =>
+     | nil => false
+     | a1 :: l1 =>
          match eq_dec a a1 with
          | left _ => true
          | right _ => mem A eq_dec a l1
          end
      end).
-
-Inductive field_rel_option (A:Type) : Type :=
-  | Field_None : field_rel_option A
-  | Field_Some : (A -> A -> A) -> field_rel_option A.
\ No newline at end of file
-- 
cgit v1.2.3