diff options
Diffstat (limited to 'theories/Strings')
| -rw-r--r-- | theories/Strings/Ascii.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index a89b888ec..7d7dcc6d0 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -10,7 +10,7 @@ (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) -Require Import Bool BinPos BinNat Nnat. +Require Import Bool BinPos BinNat PeanoNat Nnat. Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -115,7 +115,7 @@ Proof. unfold N.lt. change 256%N with (N.of_nat 256). rewrite <- Nat2N.inj_compare. - rewrite <- Compare_dec.nat_compare_lt. auto. + now apply Nat.compare_lt_iff. Qed. |