diff options
| -rw-r--r-- | backend/Duplicate.v | 3 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 2 |
2 files changed, 2 insertions, 3 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 7dea752b..40db4e45 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm := match lm with | nil => OK tt | m :: lm => do u <- verify_mapping_mn dupmap f f' m; - do u2 <- verify_mapping_mn_rec dupmap f f' lm; - OK tt + verify_mapping_mn_rec dupmap f f' lm end. Definition verify_mapping_match_nodes dupmap (f f': function): res unit := 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: |