diff options
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 5a19510a..20ba74a1 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -568,7 +568,7 @@ Proof. predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. TrivialExists. simpl in *. - unfold select. + unfold eval_select. f_equal. inv H6. inv H7. @@ -606,7 +606,7 @@ Proof. predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. TrivialExists. simpl in *. - unfold select. + unfold eval_select. f_equal. inv H6. inv H7. |