diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-06-07 19:05:24 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-06-07 19:05:24 +0200 |
| commit | e1de6a1c3c5cbf4c6551d3442e3c4e49145709fb (patch) | |
| tree | 640e443c8b598fd62ce1cfa7312ce56f8ef9ac42 | |
| parent | 47f63df0a43209570de224f28cf53da6a758df16 (diff) | |
| parent | 8dac286930288a1e7dfa39e030d58cfd5714d8d3 (diff) | |
| download | compcert-kvx-e1de6a1c3c5cbf4c6551d3442e3c4e49145709fb.tar.gz compcert-kvx-e1de6a1c3c5cbf4c6551d3442e3c4e49145709fb.zip | |
Merge pull request #185 from letouzey/no-BigNumPrelude
Do not rely on the hints of BigNumPrelude
| -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] **) |