From b7374d225af55ecc6f5d6aa8f3684bfae99ff465 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 2 Oct 2019 19:23:51 +0200 Subject: 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. --- backend/ValueAnalysis.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/ValueAnalysis.v') diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8dbb67a7..2b233900 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1148,10 +1148,10 @@ Proof. - constructor. - assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto. xomega. auto. auto. + apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. - assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto. xomega. auto. auto. + apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto. Qed. @@ -1362,7 +1362,7 @@ Proof. apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. - rewrite C; auto. + rewrite C; auto with ordered_type. exact AA. * (* public builtin call *) exploit anonymize_stack; eauto. @@ -1381,7 +1381,7 @@ Proof. apply sound_stack_exten with bc. apply sound_stack_inv with m. auto. intros. apply Q. red. eapply Plt_trans; eauto. - rewrite C; auto. + rewrite C; auto with ordered_type. exact AA. } unfold transfer_builtin in TR. -- cgit