diff options
| -rw-r--r-- | cparser/validator/Alphabet.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index 2d7f8ff9..ca71bf59 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -249,7 +249,7 @@ erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega. rewrite phi_incr, Zmod_small; intuition; try omega. apply inj_lt in H. pose proof Zle_le_succ. -do 2 rewrite inj_Zabs_nat, Zabs_eq in H; eauto. +do 2 rewrite inj_Zabs_nat, Zabs_eq in H; now eauto. Qed. (** Previous class instances for [option A] **) |