Coq 8.10 compatibility: make explicit the "core" hint database

"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".

8 files changed, 22 insertions, 23 deletions

diff --git a/backend/Conventions.v b/backend/Conventions.v
index 989bfa05..6025c6b4 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -128,8 +128,6 @@ Definition callee_save_loc (l: loc) :=
   | S sl ofs ty => sl <> Outgoing
   end.
 
-Hint Unfold callee_save_loc.
-
 Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop :=
   forall l, callee_save_loc l -> ls1 l = ls2 l.
 
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',
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 782fb32a..aa73abb0 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -1131,7 +1131,7 @@ Qed.
 Remark val_inject_vptrofs: forall n, Val.inject f (Vptrofs n) (Vptrofs n).
 Proof. intros. unfold Vptrofs. destruct Archi.ptr64; auto. Qed.
 
-Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs.
+Local Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs : core.
 
 Ltac TrivialInject :=
   match goal with
@@ -1517,7 +1517,7 @@ Inductive val_casted: val -> type -> Prop :=
   | val_casted_void: forall v,
       val_casted v Tvoid.
 
-Hint Constructors val_casted.
+Local Hint Constructors val_casted : core.
 
 Remark cast_int_int_idem:
   forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i.
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 28c8eeb8..c235031f 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -222,7 +222,7 @@ Proof.
   induction 1; constructor; auto.
 Qed.
 
-Hint Resolve leftcontext_context.
+Local Hint Resolve leftcontext_context : core.
 
 (** Strategy for reducing expressions. We reduce the leftmost innermost
   non-simple subexpression, evaluating its arguments (which are necessarily
@@ -398,8 +398,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.
 
 (** * Safe executions. *)
 
@@ -975,7 +975,7 @@ Proof.
   apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc.
 Qed.
 
-Hint Resolve contextlist'_head contextlist'_tail.
+Local Hint Resolve contextlist'_head contextlist'_tail : core.
 
 Lemma eval_simple_list_steps:
   forall rl vl, eval_simple_list' rl vl ->
@@ -1049,7 +1049,7 @@ Scheme expr_ind2 := Induction for expr Sort Prop
   with exprlist_ind2 := Induction for exprlist Sort Prop.
 Combined Scheme expr_expr_list_ind from expr_ind2, exprlist_ind2.
 
-Hint Constructors leftcontext leftcontextlist.
+Local Hint Constructors leftcontext leftcontextlist : core.
 
 Lemma decompose_expr:
   (forall a from C,
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 37e2cd96..e7d57a1c 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -687,7 +687,7 @@ Hint Resolve gensym_within within_widen contained_widen
              in_eq in_cons
              Ple_trans Ple_refl: gensym.
 
-Hint Resolve dest_for_val_below dest_for_effect_below.
+Local Hint Resolve dest_for_val_below dest_for_effect_below : core.
 
 (** ** Correctness of the translation functions *)
 
diff --git a/common/Separation.v b/common/Separation.v
index 1493b535..27065d1f 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -113,7 +113,7 @@ Proof.
   intros P Q [[A B] [C D]]. split; auto.
 Qed.
 
-Hint Resolve massert_imp_refl massert_eqv_refl.
+Hint Resolve massert_imp_refl massert_eqv_refl : core.
 
 (** * Separating conjunction *)
 
diff --git a/common/Values.v b/common/Values.v
index a51a390f..2eb778a5 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1949,7 +1949,7 @@ Inductive lessdef_list: list val -> list val -> Prop :=
       lessdef v1 v2 -> lessdef_list vl1 vl2 ->
       lessdef_list (v1 :: vl1) (v2 :: vl2).
 
-Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.
+Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
 
 Lemma lessdef_list_inv:
   forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.
@@ -2174,7 +2174,7 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
   | val_inject_undef: forall v,
       inject mi Vundef v.
 
-Hint Constructors inject.
+Hint Constructors inject : core.
 
 Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
   | inject_list_nil :
@@ -2183,7 +2183,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
       inject mi v v' -> inject_list mi vl vl'->
       inject_list mi (v :: vl) (v' :: vl').
 
-Hint Resolve inject_list_nil inject_list_cons.
+Hint Resolve inject_list_nil inject_list_cons : core.
 
 Lemma inject_ptrofs:
   forall mi i, inject mi (Vptrofs i) (Vptrofs i).
@@ -2191,7 +2191,7 @@ Proof.
   unfold Vptrofs; intros. destruct Archi.ptr64; auto.
 Qed.
 
-Hint Resolve inject_ptrofs.
+Hint Resolve inject_ptrofs : core.
 
 Section VAL_INJ_OPS.
 
@@ -2494,7 +2494,7 @@ Proof.
   constructor. eapply val_inject_incr; eauto. auto.
 Qed.
 
-Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr.
+Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
 
 Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.
diff --git a/lib/Floats.v b/lib/Floats.v
index 7677e3c8..13350dd0 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -139,8 +139,8 @@ Definition default_nan_32 := quiet_nan_32 Archi.default_nan_32.
 
 Local Notation __ := (eq_refl Datatypes.Lt).
 
-Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt).
-Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt).
+Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt) : core.
+Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt) : core.
 
 (** * Double-precision FP numbers *)