diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /cparser/validator/Alphabet.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'cparser/validator/Alphabet.v')
| -rw-r--r-- | cparser/validator/Alphabet.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index 85a1689d..13718cd5 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -193,7 +193,7 @@ Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := { AlphabetComparable := {| compare := fun x y => compare31 (inj x) (inj y) |}; AlphabetFinite := - {| all_list := fst (iter_int31 inj_bound _ + {| all_list := fst (iter_int31 inj_bound _ (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }. Next Obligation. apply Zcompare_antisym. Qed. Next Obligation. @@ -229,7 +229,7 @@ rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; refle replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega. rewrite Z_mod_same_full in H0. exfalso; omega. -exfalso; inversion Heqp; subst; +exfalso; inversion Heqp; subst; pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega. clear H. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. |