From d4e2f7b715b21efe0d693415ab63dad5a22afa92 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Oct 2019 18:34:30 +0200 Subject: eq_condition already existed --- backend/Duplicateproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 54dd6196..d16505dd 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -132,7 +132,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 *) -- cgit