From e1cad068ffc188d06c37f46e1bf6e7b57e02e219 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 17 Dec 2010 21:00:26 +0000
Subject: Cosmetic : let's take advantage of the n-ary exists notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13721 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/Ndigits.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/NArith')

diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 5b3157143..a5d6b6730 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -208,7 +208,7 @@ Proof.
 Qed.
 
 Lemma Ntestbit_spec : forall a n,
-  exists l, exists h, 0<=l<2^n /\
+  exists l h, 0<=l<2^n /\
     a = l + ((if Ntestbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros [|a] n.
-- 
cgit v1.2.3