diff options
Diffstat (limited to 'backend/Duplicateproof.v')
-rw-r--r-- | backend/Duplicateproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index da6d24d0..04936eeb 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -165,7 +165,7 @@ Proof. - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_correct in EQ. destruct x0. eapply verify_is_copy_correct in EQ1. - destruct (condition_eq _ _); try discriminate. + destruct (eq_condition _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption. (* Ijumptable *) |