diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
| commit | 5664fddcab15ef4482d583673c75e07bd1e96d0a (patch) | |
| tree | 878b22860e69405ba5cf6fd2798731dac8ce660c /cparser/validator/Alphabet.v | |
| parent | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff) | |
| parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
| download | compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip | |
Merge remote-tracking branch 'origin/master' into parser_fix
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. |