From 6f737edae4b7e6243a9f11e74614f55381f62ec7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 2 Aug 2019 10:41:29 +0200 Subject: Coq 8.10 compatibility: make explicit the "core" hint database "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". --- cfrontend/Cexec.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index e6bf2129..2942080b 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1124,8 +1124,8 @@ Proof. induction 1; intros; constructor; eauto. Qed. -Hint Constructors context contextlist. -Hint Resolve context_compose contextlist_compose. +Local Hint Constructors context contextlist : core. +Local Hint Resolve context_compose contextlist_compose : core. Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := match k, rd with @@ -1691,8 +1691,9 @@ Proof. change (In (f (C0, rd)) (map f res2)). apply in_map; auto. Qed. -Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval - reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right. +Local Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval + reducts_incl_incontext reducts_incl_incontext2_left + reducts_incl_incontext2_right : core. Lemma step_expr_context: forall from to C, context from to C -> @@ -2077,7 +2078,7 @@ Ltac myinv := | _ => idtac end. -Hint Extern 3 => exact I. +Local Hint Extern 3 => exact I : core. Theorem do_step_sound: forall w S rule t S', -- cgit