Commit b58712b7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Partly fix compilation with Coq 8.8.

parent 66646a13
...@@ -643,6 +643,11 @@ if test "$enable_coq_support" = yes; then ...@@ -643,6 +643,11 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma" COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION) AC_MSG_RESULT($COQVERSION)
;; ;;
8.8*)
coq_compat_version="COQ88"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*) *)
enable_coq_support=no enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded) AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
......
...@@ -1940,6 +1940,7 @@ Lemma nth_bit_pred_high : ...@@ -1940,6 +1940,7 @@ Lemma nth_bit_pred_high :
to_uint i < size -> to_uint i < size ->
to_uint i < Z.of_nat n -> to_uint i < Z.of_nat n ->
nth_bv (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) i = true. nth_bv (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) i = true.
Proof.
induction n;intros. induction n;intros.
assert (Z.of_nat 0 <= to_uint i) by apply to_uint_bounds. assert (Z.of_nat 0 <= to_uint i) by apply to_uint_bounds.
omega. omega.
...@@ -1955,8 +1956,8 @@ Lemma nth_bit_pred_high : ...@@ -1955,8 +1956,8 @@ Lemma nth_bit_pred_high :
case (Z_lt_le_dec (to_uint i) 1); intro. case (Z_lt_le_dec (to_uint i) 1); intro.
right. right.
assert (to_uint i = 0). assert (to_uint i = 0).
pose (to_uint_bounds i). assert (H' := to_uint_bounds i).
auto with zarith. omega.
rewrite H1; apply nth_zeros_is_hd. rewrite H1; apply nth_zeros_is_hd.
left. left.
...@@ -2044,10 +2045,11 @@ Lemma mask_correctness : ...@@ -2044,10 +2045,11 @@ Lemma mask_correctness :
forall (j:Z), forall (j:Z),
(j < size -> (to_uint i) <= j -> j < (to_uint i + to_uint n)%Z -> nth mask j = true) (j < size -> (to_uint i) <= j -> j < (to_uint i + to_uint n)%Z -> nth mask j = true)
/\ (j < to_uint i \/ j >= to_uint i + to_uint n -> nth mask j = false). /\ (j < to_uint i \/ j >= to_uint i + to_uint n -> nth mask j = false).
Proof.
split;intros. split;intros.
rewrite lsl_bv_is_lsl. rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i). assert (a := to_uint_bounds i).
pose (size_in_range). assert (u := size_in_range).
rewrite uint_in_range_power in u. rewrite uint_in_range_power in u.
rewrite Lsl_nth_high; auto with zarith. rewrite Lsl_nth_high; auto with zarith.
assert (j - to_uint i = to_uint (sub (of_int j) i)). assert (j - to_uint i = to_uint (sub (of_int j) i)).
...@@ -2066,8 +2068,8 @@ Lemma mask_correctness : ...@@ -2066,8 +2068,8 @@ Lemma mask_correctness :
apply Lsl_nth_low; auto with zarith. apply Lsl_nth_low; auto with zarith.
rewrite lsl_bv_is_lsl. rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i) as u. assert (u := to_uint_bounds i).
pose (to_uint_bounds n) as v. assert (v := to_uint_bounds n).
pose size_in_range as w; rewrite uint_in_range_power in w. pose size_in_range as w; rewrite uint_in_range_power in w.
assert (0 <= j) by auto with zarith. assert (0 <= j) by auto with zarith.
...@@ -2095,6 +2097,7 @@ Qed. ...@@ -2095,6 +2097,7 @@ Qed.
Lemma eq_sub_equiv : Lemma eq_sub_equiv :
forall (a:t) (b:t) (i:t) (n:t), forall (a:t) (b:t) (i:t) (n:t),
(eq_sub a b (to_uint i) (to_uint n)) <-> (eq_sub_bv a b i n). (eq_sub a b (to_uint i) (to_uint n)) <-> (eq_sub_bv a b i n).
Proof.
intros a b i n. intros a b i n.
unfold eq_sub, eq_sub_bv. unfold eq_sub, eq_sub_bv.
transitivity (eq_aux (bw_and b (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i)) transitivity (eq_aux (bw_and b (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i))
...@@ -2119,7 +2122,7 @@ Lemma eq_sub_equiv : ...@@ -2119,7 +2122,7 @@ Lemma eq_sub_equiv :
case (Z_lt_ge_dec j size); intro. case (Z_lt_ge_dec j size); intro.
pose (to_uint_bounds i) as u; unfold uint_in_range in u. assert (u := to_uint_bounds i); unfold uint_in_range in u.
assert (0 <= j < Z.of_nat size_nat) by auto with zarith. assert (0 <= j < Z.of_nat size_nat) by auto with zarith.
pose (H j H1). pose (H j H1).
fold nth in e; rewrite Nth_bw_and, Nth_bw_and in e by auto. fold nth in e; rewrite Nth_bw_and, Nth_bw_and in e by auto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment