diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2021-01-06 21:32:08 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2021-01-06 21:33:17 +0100 |
| commit | d82f294dcc879acad5fb7e2d2fd4a48070f3f04d (patch) | |
| tree | 36abee31da6f635ea21684a61b414f71616ec9a6 /backend/Duplicateproof.v | |
| parent | 6a77f39a8e8ea383ddfa76cbe444b93ef5501429 (diff) | |
| download | compcert-kvx-d82f294dcc879acad5fb7e2d2fd4a48070f3f04d.tar.gz compcert-kvx-d82f294dcc879acad5fb7e2d2fd4a48070f3f04d.zip | |
Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231
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 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: |