diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |