diff options
Diffstat (limited to 'cfrontend/Cexec.v')
| -rw-r--r-- | cfrontend/Cexec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index e063dfc3..823d2542 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -513,8 +513,8 @@ Definition do_external (ef: external_function): | EF_malloc => do_ef_malloc | EF_free => do_ef_free | EF_memcpy sz al => do_ef_memcpy sz al - | EF_annot text targs => do_ef_annot text targs - | EF_annot_val text targ => do_ef_annot_val text targ + | EF_annot kind text targs => do_ef_annot text targs + | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs end. @@ -1770,7 +1770,7 @@ Lemma not_stuckred_imm_safe: Proof. intros. generalize (step_expr_sound a k m). intros [A B]. destruct (step_expr k a m) as [|[C rd] res] eqn:?. - specialize (B (refl_equal _)). destruct k. + specialize (B (eq_refl _)). destruct k. destruct a; simpl in B; try congruence. constructor. destruct a; simpl in B; try congruence. constructor. assert (NOTSTUCK: rd <> Stuckred). |