diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-10-02 19:23:51 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-10-02 19:23:51 +0200 |
| commit | b7374d225af55ecc6f5d6aa8f3684bfae99ff465 (patch) | |
| tree | 75a9858d151984c2033c66fa171bed3305fa20ce /backend/Inliningproof.v | |
| parent | ca5f8a7629a6e31cc287139ad0a69b8154514260 (diff) | |
| download | compcert-kvx-b7374d225af55ecc6f5d6aa8f3684bfae99ff465.tar.gz compcert-kvx-b7374d225af55ecc6f5d6aa8f3684bfae99ff465.zip | |
Make explicit the use of hints from OrderedType (#316)
Some hints will move from the core database to the `ordered_type` database
(see https://github.com/coq/coq/pull/9772).
This commit prepares for this move by adding `with ordered_type` to the invocations
of `auto` and `eauto` that use the hints in question.
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 181f40bf..cc84b1cc 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -744,7 +744,7 @@ Lemma match_stacks_free_right: match_stacks F m m1' stk stk' sp. Proof. intros. eapply match_stacks_invariant; eauto. - intros. eapply Mem.perm_free_1; eauto. + intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. Qed. @@ -1043,7 +1043,7 @@ Proof. eapply match_stacks_bound with (bound := sp'). eapply match_stacks_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. - intros. eapply Mem.perm_free_1; eauto. + intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. erewrite Mem.nextblock_free; eauto. red in VB; xomega. eapply agree_val_regs; eauto. @@ -1135,7 +1135,7 @@ Proof. eapply match_stacks_bound with (bound := sp'). eapply match_stacks_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. - intros. eapply Mem.perm_free_1; eauto. + intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. erewrite Mem.nextblock_free; eauto. red in VB; xomega. destruct or; simpl. apply agree_val_reg; auto. auto. @@ -1182,7 +1182,7 @@ Proof. subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto. intros. eapply Mem.perm_alloc_1; eauto. intros. exploit Mem.perm_alloc_inv. eexact A. eauto. - rewrite dec_eq_false; auto. + rewrite dec_eq_false; auto with ordered_type. auto. auto. auto. eauto. auto. rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto. eapply Mem.valid_new_block; eauto. |