From 241b8e65f626fafd866e952377b47403fb654d1b Mon Sep 17 00:00:00 2001
From: marche
Date: Tue, 10 Feb 2004 15:38:01 +0000
Subject: backtrack implicit dans Bvector

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5312 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bvector.v   | 2 ++
 theories/ZArith/Zbinary.v | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index aa69fccf12..75db13172f 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -196,8 +196,10 @@ Defined.
 
 End VECTORS.
 
+(* suppressed: incompatible with Coq-Art book 
 Implicit Arguments Vnil [A].
 Implicit Arguments Vcons [A n].
+*)
 
 Section BOOLEAN_VECTORS.
 
diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v
index c78e0a72f6..92fa6097c1 100644
--- a/theories/ZArith/Zbinary.v
+++ b/theories/ZArith/Zbinary.v
@@ -186,7 +186,7 @@ Meriterait d'etre reecrite.
 
 Lemma binary_value_Sn :
  forall (n:nat) (b:bool) (bv:Bvector n),
-   binary_value (S n) (Vcons b bv) =
+   binary_value (S n) (Vcons bool b n bv) =
    (bit_value b + 2 * binary_value n bv)%Z.
 Proof.
 	intros; auto.
-- 
cgit v1.2.3