From c709a9a54d07fcfd1d18418a0a234804a80e0484 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 7 Nov 2019 12:26:15 +0100 Subject: [PATCH] Put global hints in `core`. --- theories/lang/lifting.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v index 2daa85ad..a174b301 100644 --- a/theories/lang/lifting.v +++ b/theories/lang/lifting.v @@ -29,12 +29,12 @@ Ltac inv_bin_op_eval := | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/= end. -Local Hint Extern 0 (atomic _) => solve_atomic. -Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl. +Local Hint Extern 0 (atomic _) => solve_atomic : core. +Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core. -Local Hint Constructors head_step bin_op_eval lit_neq lit_eq. -Local Hint Resolve alloc_fresh. -Local Hint Resolve to_of_val. +Local Hint Constructors head_step bin_op_eval lit_neq lit_eq : core. +Local Hint Resolve alloc_fresh : core. +Local Hint Resolve to_of_val : core. Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) := as_rec : e = Rec f xl erec. -- GitLab