From e7da402f36d030484d11960cf12581fd1c1f159a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 7 Oct 2019 14:51:43 +0200 Subject: Ireturn --- backend/Duplicateproof.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backend/Duplicateproof.v') diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 7369c3ea..37c583df 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -121,6 +121,10 @@ Proof. destruct (builtin_res_eq_pos _ _); try discriminate. eapply verify_is_copy_correct_one. destruct x. eassumption. subst. constructor. +(* Ireturn *) + - destruct i'; try (inversion H; fail). + destruct (option_eq _ _ _); try discriminate. subst. clear H. + constructor. Qed. Lemma verify_mapping_mn_correct: -- cgit