diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:08:33 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:17:50 +0200 |
| commit | 136986c204af19341aeb455d72fe817b16fa6fff (patch) | |
| tree | 02e9178d9f2cf942bd32366891d480ff161406f6 /cparser/validator/Alphabet.v | |
| parent | c46723c0169145d41d1879c236f53314456f1ba1 (diff) | |
| parent | 1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 (diff) | |
| download | compcert-136986c204af19341aeb455d72fe817b16fa6fff.tar.gz compcert-136986c204af19341aeb455d72fe817b16fa6fff.zip | |
Merge remote branch 'upstream/master' into clean
Conflicts:
Makefile.extr
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. |