From 8e4ba92321576e92dbe91b014287d3981447df98 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 17 May 2006 10:43:13 +0000
Subject: Typo dans List.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8826 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/List.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4fe83e9804..79d5a95b03 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -517,7 +517,7 @@ Section Elts.
   (** ** Counting occurences of a element *)
   (****************************************)
 
-  Axiom eqA_dec : forall x y : A, {x = y}+{x <> y}.
+  Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
   
   Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
     match l with 
@@ -961,6 +961,8 @@ Section ListOps.
   (** ** Decidable equality on lists *)
   (***********************************)
 
+  Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}.
+
   Lemma list_eq_dec :
     forall l l':list A, {l = l'} + {l <> l'}.
   Proof.
-- 
cgit v1.2.3