diff options
| author | Jasper Hugunin | 2020-10-09 16:33:49 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | 5a3d6f1d2c193be514e610779b80829eef4fe4a8 (patch) | |
| tree | 92a2aceaf01ead08f99e588df1bb264bc8337abf | |
| parent | 4d4d2128d2dc761a1b3e002780b865f77fe61e67 (diff) | |
Modify Strings/Ascii.v to compile with -mangle-names
| -rw-r--r-- | theories/Strings/Ascii.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index c155395ecd..06b02ab211 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -128,28 +128,28 @@ Definition nat_of_ascii (a : ascii) : nat := N.to_nat (N_of_ascii a). Theorem ascii_N_embedding : forall a : ascii, ascii_of_N (N_of_ascii a) = a. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. Qed. Theorem N_ascii_embedding : forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n. Proof. -destruct n. +intro n; destruct n as [|p]. reflexivity. -do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]); +do 8 (destruct p as [p|p|]; [ | | intros; vm_compute; reflexivity ]); intro H; vm_compute in H; destruct p; discriminate. Qed. Theorem N_ascii_bounded : forall a : ascii, (N_of_ascii a < 256)%N. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity. Qed. Theorem ascii_nat_embedding : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a. Proof. - destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. + intro a; destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity. Qed. Theorem nat_ascii_embedding : |