From d82f294dcc879acad5fb7e2d2fd4a48070f3f04d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 6 Jan 2021 21:32:08 +0100 Subject: Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231 --- 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 2480ccf0..cc24104f 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -111,7 +111,7 @@ Proof. - monadInv H0. inversion H. - inversion H. + subst. monadInv H0. destruct x. assumption. - + monadInv H0. destruct x0. eapply IHlb; assumption. + + monadInv H0. destruct x. eapply IHlb; assumption. Qed. Lemma verify_is_copy_correct: -- cgit