From 8dac286930288a1e7dfa39e030d58cfd5714d8d3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 6 Jun 2017 17:50:04 +0200 Subject: Alphabet.v compiles even without the hints of BigNumPrelude BigNumPrelude will soon leave Coq stdlib with the rest of the bignum library (apart from Int31 files) to become a separate package. With this (very minor) patch, Compcert compiles with or without the hints declared in BigNumPrelude. --- cparser/validator/Alphabet.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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] **) -- cgit