Fix warnings for Coq 8.13.2

10 files changed, 84 insertions, 70 deletions

diff --git a/docs b/docs
-Subproject 42e19f2b20c907505a28486a8071147ed6c610f
+Subproject f85238030a96a082f19446a7998da97123ce702
diff --git a/src/common/Monad.v b/src/common/Monad.v
index 5e8385e..fcbe527 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -40,10 +40,10 @@ Module MonadExtra(M : Monad).
 
     Notation "'do' X <- A ; B" :=
       (bind A (fun X => B))
-        (at level 200, X ident, A at level 100, B at level 200).
+        (at level 200, X name, A at level 100, B at level 200).
     Notation "'do' ( X , Y ) <- A ; B" :=
       (bind2 A (fun X Y => B))
-        (at level 200, X ident, Y ident, A at level 100, B at level 200).
+        (at level 200, X name, Y name, A at level 100, B at level 200).
 
   End MonadNotation.
   Import MonadNotation.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index b58ebd4..389a74f 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -34,7 +34,7 @@ Require Import vericert.common.Show.
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
 
-Local Open Scope Z_scope.
+#[local] Open Scope Z_scope.
 
 (* This tactic due to Clement Pit-Claudel with some minor additions by JDP to
    allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *)
@@ -190,8 +190,8 @@ Ltac liapp :=
 Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
               try assumption; try (solve [auto]).
 
-Global Opaque Nat.div.
-Global Opaque Z.mul.
+#[global] Opaque Nat.div.
+#[global] Opaque Z.mul.
 
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
@@ -231,7 +231,7 @@ Definition join {A : Type} (a : option (option A)) : option A :=
 
 Module Notation.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X ident, A at level 100, B at level 200).
+   (at level 200, X name, A at level 100, B at level 200).
 End Notation.
 
 End Option.
diff --git a/src/hls/Array.v b/src/hls/Array.v
index dec1335..0f5ae02 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -51,7 +51,7 @@ Lemma list_set_spec1 {A : Type} :
 Proof.
   induction l; intros; destruct i; crush; firstorder. intuition.
 Qed.
-Hint Resolve list_set_spec1 : array.
+#[export] Hint Resolve list_set_spec1 : array.
 
 Lemma list_set_spec2 {A : Type} :
   forall l i (x : A) d,
@@ -59,7 +59,7 @@ Lemma list_set_spec2 {A : Type} :
 Proof.
   induction l; intros; destruct i; crush; firstorder. intuition.
 Qed.
-Hint Resolve list_set_spec2 : array.
+#[export] Hint Resolve list_set_spec2 : array.
 
 Lemma list_set_spec3 {A : Type} :
   forall l i1 i2 (x : A),
@@ -68,7 +68,7 @@ Lemma list_set_spec3 {A : Type} :
 Proof.
   induction l; intros; destruct i1; destruct i2; crush; firstorder.
 Qed.
-Hint Resolve list_set_spec3 : array.
+#[export] Hint Resolve list_set_spec3 : array.
 
 Lemma array_set_wf {A : Type} :
   forall l ln i (x : A),
@@ -95,7 +95,7 @@ Proof.
   unfold array_set. crush.
   eauto with array.
 Qed.
-Hint Resolve array_set_spec1 : array.
+#[export] Hint Resolve array_set_spec1 : array.
 
 Lemma array_set_spec2 {A : Type} :
   forall a i (x : A) d,
@@ -107,7 +107,7 @@ Proof.
   unfold array_set. crush.
   eauto with array.
 Qed.
-Hint Resolve array_set_spec2 : array.
+#[export] Hint Resolve array_set_spec2 : array.
 
 Lemma array_set_len {A : Type} :
   forall a i (x : A),
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 98eda9c..8dbc6b2 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -29,9 +29,8 @@ Module AssocMap := Maps.PTree.
 Module AssocMapExt.
   Import AssocMap.
 
-  Hint Resolve elements_correct elements_complete
-       elements_keys_norepet : assocmap.
-  Hint Resolve gso gss : assocmap.
+  #[export] Hint Resolve elements_correct elements_complete elements_keys_norepet : assocmap.
+  #[export] Hint Resolve gso gss : assocmap.
 
   Section Operations.
 
@@ -55,7 +54,6 @@ Module AssocMapExt.
       forall am,
       merge (empty A) am = am.
     Proof. auto. Qed.
-    Hint Resolve merge_base_1 : assocmap.
 
     Lemma merge_base_2 :
       forall am,
@@ -65,7 +63,6 @@ Module AssocMapExt.
       destruct am; trivial.
       destruct o; trivial.
     Qed.
-    Hint Resolve merge_base_2 : assocmap.
 
     Lemma merge_add_assoc :
       forall r am am' v,
@@ -74,7 +71,6 @@ Module AssocMapExt.
       induction r; intros; destruct am; destruct am'; try (destruct o); simpl;
         try rewrite IHr; try reflexivity.
     Qed.
-    Hint Resolve merge_add_assoc : assocmap.
 
     Lemma merge_correct_1 :
       forall am bm k v,
@@ -84,7 +80,6 @@ Module AssocMapExt.
       induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
         try rewrite gempty in H; try discriminate; try assumption; auto.
     Qed.
-    Hint Resolve merge_correct_1 : assocmap.
 
     Lemma merge_correct_2 :
       forall am bm k v,
@@ -95,7 +90,6 @@ Module AssocMapExt.
       induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
         try rewrite gempty in H; try discriminate; try assumption; auto.
     Qed.
-    Hint Resolve merge_correct_2 : assocmap.
 
     Lemma merge_correct_3 :
       forall am bm k,
@@ -106,7 +100,6 @@ Module AssocMapExt.
       induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
         try rewrite gempty in H; try discriminate; try assumption; auto.
     Qed.
-    Hint Resolve merge_correct_3 : assocmap.
 
     Definition merge_fold (am bm : t A) : t A :=
       fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).
@@ -130,7 +123,6 @@ Module AssocMapExt.
           apply IHl. contradiction. contradiction.
           simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption.
     Qed.
-    Hint Resolve add_assoc : assocmap.
 
     Lemma not_in_assoc :
       forall k v l bm,
@@ -145,7 +137,6 @@ Module AssocMapExt.
           simpl in *; apply Decidable.not_or in H; destruct H. contradiction.
         rewrite AssocMap.gso; auto.
     Qed.
-    Hint Resolve not_in_assoc : assocmap.
 
     Lemma elements_iff :
       forall am k,
@@ -158,14 +149,22 @@ Module AssocMapExt.
       exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing.
       rewrite H in H0; assumption.
     Qed.
-    Hint Resolve elements_iff : assocmap.
+
+    #[local] Hint Resolve merge_base_1 : core.
+    #[local] Hint Resolve merge_base_2 : core.
+    #[local] Hint Resolve merge_add_assoc : core.
+    #[local] Hint Resolve merge_correct_1 : core.
+    #[local] Hint Resolve merge_correct_2 : core.
+    #[local] Hint Resolve merge_correct_3 : core.
+    #[local] Hint Resolve add_assoc : core.
+    #[local] Hint Resolve not_in_assoc : core.
+    #[local] Hint Resolve elements_iff : core.
 
     Lemma elements_correct' :
       forall am k,
       ~ (exists v, get k am = Some v) <->
       ~ List.In k (List.map (@fst _ A) (elements am)).
-    Proof. auto using not_iff_compat with assocmap. Qed.
-    Hint Resolve elements_correct' : assocmap.
+    Proof. auto using not_iff_compat. Qed.
 
     Lemma elements_correct_none :
       forall am k,
@@ -175,31 +174,46 @@ Module AssocMapExt.
       intros. apply elements_correct'. unfold not. intros.
       destruct H0. rewrite H in H0. discriminate.
     Qed.
-    Hint Resolve elements_correct_none : assocmap.
 
     Lemma merge_fold_add :
       forall k v am bm,
       am ! k = Some v ->
       (merge_fold am bm) ! k = Some v.
     Proof. unfold merge_fold; auto with assocmap. Qed.
-    Hint Resolve merge_fold_add : assocmap.
+
+    #[local] Hint Resolve elements_correct' : core.
+    #[local] Hint Resolve elements_correct_none : core.
+    #[local] Hint Resolve merge_fold_add : core.
 
     Lemma merge_fold_not_in :
       forall k v am bm,
       get k am = None ->
       get k bm = Some v ->
       get k (merge_fold am bm) = Some v.
-    Proof. intros. apply not_in_assoc; auto with assocmap. Qed.
-    Hint Resolve merge_fold_not_in : assocmap.
+    Proof. intros. apply not_in_assoc; auto. Qed.
 
     Lemma merge_fold_base :
       forall am,
       merge_fold (empty A) am = am.
     Proof. auto. Qed.
-    Hint Resolve merge_fold_base : assocmap.
 
   End Operations.
 
+  #[export] Hint Resolve merge_base_1 : assocmap.
+  #[export] Hint Resolve merge_base_2 : assocmap.
+  #[export] Hint Resolve merge_add_assoc : assocmap.
+  #[export] Hint Resolve merge_correct_1 : assocmap.
+  #[export] Hint Resolve merge_correct_2 : assocmap.
+  #[export] Hint Resolve merge_correct_3 : assocmap.
+  #[export] Hint Resolve add_assoc : assocmap.
+  #[export] Hint Resolve not_in_assoc : assocmap.
+  #[export] Hint Resolve elements_iff : assocmap.
+  #[export] Hint Resolve elements_correct' : assocmap.
+  #[export] Hint Resolve merge_fold_not_in : assocmap.
+  #[export] Hint Resolve merge_fold_base : assocmap.
+  #[export] Hint Resolve elements_correct_none : assocmap.
+  #[export] Hint Resolve merge_fold_add : assocmap.
+
 End AssocMapExt.
 Import AssocMapExt.
 
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 61ea541..8cebbfd 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -227,7 +227,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       mst = mod_st m ->
       step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
            (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
-Hint Constructors step : htl.
+#[export] Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro: forall b m0 m,
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 4d60a24..3f4e513 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -33,11 +33,11 @@ Require Import vericert.hls.HTL.
 Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
 
-Hint Resolve AssocMap.gempty : htlh.
-Hint Resolve AssocMap.gso : htlh.
-Hint Resolve AssocMap.gss : htlh.
-Hint Resolve Ple_refl : htlh.
-Hint Resolve Ple_succ : htlh.
+#[local] Hint Resolve AssocMap.gempty : htlh.
+#[local] Hint Resolve AssocMap.gso : htlh.
+#[local] Hint Resolve AssocMap.gss : htlh.
+#[local] Hint Resolve Ple_refl : htlh.
+#[local] Hint Resolve Ple_succ : htlh.
 
 Record state: Type := mkstate {
   st_st : reg;
@@ -74,10 +74,10 @@ Module HTLState <: State.
             s1.(st_controllogic)!n = None
             \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
         st_incr s1 s2.
-  Hint Constructors st_incr : htlh.
+  #[export] Hint Constructors st_incr : htlh.
 
   Definition st_prop := st_incr.
-  Hint Unfold st_prop : htlh.
+  #[export] Hint Unfold st_prop : htlh.
 
   Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
 
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 679f5ec..098eef1 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -146,7 +146,7 @@ Lemma contradictory_assignment : forall s l cl a,
   tauto.
 Qed.
 
-Local Hint Resolve contradictory_assignment : core.
+#[local] Hint Resolve contradictory_assignment : core.
 
 (** Augment an assignment with a new mapping. *)
 Definition upd (a : asgn) (l : lit) : asgn :=
@@ -163,7 +163,7 @@ Lemma satLit_upd_eq : forall l a,
   destruct (eq_nat_dec (snd l) (snd l)); tauto.
 Qed.
 
-Local Hint Resolve satLit_upd_eq : core.
+#[local] Hint Resolve satLit_upd_eq : core.
 
 Lemma satLit_upd_neq : forall v l s a,
   v <> snd l
@@ -173,7 +173,7 @@ Lemma satLit_upd_neq : forall v l s a,
   destruct (eq_nat_dec v (snd l)); tauto.
 Qed.
 
-Local Hint Resolve satLit_upd_neq : core.
+#[local] Hint Resolve satLit_upd_neq : core.
 
 Lemma satLit_upd_neq2 : forall v l s a,
   v <> snd l
@@ -183,7 +183,7 @@ Lemma satLit_upd_neq2 : forall v l s a,
   destruct (eq_nat_dec v (snd l)); tauto.
 Qed.
 
-Local Hint Resolve satLit_upd_neq2 : core.
+#[local] Hint Resolve satLit_upd_neq2 : core.
 
 Lemma satLit_contra : forall s l a cl,
   s <> fst l
@@ -194,7 +194,7 @@ Lemma satLit_contra : forall s l a cl,
   assert False; intuition.
 Qed.
 
-Local Hint Resolve satLit_contra : core.
+#[local] Hint Resolve satLit_contra : core.
 
 (** Here's the tactic that I used to discharge #<i>#all#</i># proof obligations
   in my implementations of the four functions you will define.
@@ -288,7 +288,7 @@ Lemma satLit_idem_lit : forall l a l',
   destruct (eq_nat_dec (snd l') (snd l)); congruence.
 Qed.
 
-Local Hint Resolve satLit_idem_lit : core.
+#[local] Hint Resolve satLit_idem_lit : core.
 
 Lemma satLit_idem_clause : forall l a cl,
   satLit l a
@@ -297,7 +297,7 @@ Lemma satLit_idem_clause : forall l a cl,
   induction cl; simpl; intuition.
 Qed.
 
-Local Hint Resolve satLit_idem_clause : core.
+#[local] Hint Resolve satLit_idem_clause : core.
 
 Lemma satLit_idem_formula : forall l a fm,
   satLit l a
@@ -306,7 +306,7 @@ Lemma satLit_idem_formula : forall l a fm,
   induction fm; simpl; intuition.
 Qed.
 
-Local Hint Resolve satLit_idem_formula : core.
+#[local] Hint Resolve satLit_idem_formula : core.
 
 (** Challenge 2: Write this function that updates an entire formula to reflect
   setting a literal to true.
@@ -349,7 +349,7 @@ Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0).
 Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0).
 Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0).*)
 
-Local Hint Extern 1 False => discriminate : core.
+#[local] Hint Extern 1 False => discriminate : core.
 
 Local Hint Extern 1 False =>
   match goal with
@@ -366,7 +366,7 @@ Definition findUnitClause : forall (fm: formula),
             match fm with
             | nil => inright _
             | (l :: nil) :: fm' => inleft (exist _ l _)
-            | cl :: fm' =>
+            | _ :: fm' =>
               match findUnitClause fm' with
               | inleft (exist _ l _) => inleft (exist _ l _)
               | inright H => inright _
@@ -387,7 +387,7 @@ Lemma unitClauseTrue : forall l a fm,
   inversion H; subst; simpl in H0; intuition.
 Qed.
 
-Local Hint Resolve unitClauseTrue : core.
+#[local] Hint Resolve unitClauseTrue : core.
 
 (** Final challenge: Implement unit propagation.  The return type of
   [unitPropagate] signifies that three results are possible:
@@ -447,7 +447,7 @@ Definition chooseSplit (fm : formula) :=
 
 Definition negate (l : lit) := (negb (fst l), snd l).
 
-Local Hint Unfold satFormula : core.
+#[local] Hint Unfold satFormula : core.
 
 Lemma satLit_dec : forall l a,
   {satLit l a} + {satLit (negate l) a}.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 1dc7e99..cee1d60 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -414,7 +414,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       expr_runp fext reg stack fs vf ->
       valueToBool vc = false ->
       expr_runp fext reg stack (Vternary c ts fs) vf.
-Hint Constructors expr_runp : verilog.
+#[export] Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
   : res A :=
@@ -512,7 +512,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations ->
     stmnt_runp f asr asa
                  (Vnonblock lhs rhs)
                  asr (nonblock_arr r i asa rhsval).
-Hint Constructors stmnt_runp : verilog.
+#[export] Hint Constructors stmnt_runp : verilog.
 
 Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
                      module_item -> reg_associations -> arr_associations -> Prop :=
@@ -526,7 +526,7 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations ->
 | mi_stepp_Vdecl :
     forall f sr0 sa0 d,
     mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0.
-Hint Constructors mi_stepp : verilog.
+#[export] Hint Constructors mi_stepp : verilog.
 
 Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations ->
                              module_item -> reg_associations -> arr_associations -> Prop :=
@@ -540,7 +540,7 @@ Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations ->
 | mi_stepp_negedge_Vdecl :
     forall f sr0 sa0 d,
     mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0.
-Hint Constructors mi_stepp : verilog.
+#[export] Hint Constructors mi_stepp : verilog.
 
 Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
                       list module_item -> reg_associations -> arr_associations -> Prop :=
@@ -552,7 +552,7 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations ->
 | mis_stepp_Nil :
     forall f sr sa,
     mis_stepp f sr sa nil sr sa.
-Hint Constructors mis_stepp : verilog.
+#[export] Hint Constructors mis_stepp : verilog.
 
 Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations ->
                       list module_item -> reg_associations -> arr_associations -> Prop :=
@@ -564,7 +564,7 @@ Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations ->
 | mis_stepp_negedge_Nil :
     forall f sr sa,
     mis_stepp_negedge f sr sa nil sr sa.
-Hint Constructors mis_stepp : verilog.
+#[export] Hint Constructors mis_stepp : verilog.
 
 Local Close Scope error_monad_scope.
 
@@ -620,7 +620,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
          (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
-Hint Constructors step : verilog.
+#[export] Hint Constructors step : verilog.
 
 Inductive initial_state (p: program): state -> Prop :=
   | initial_state_intro: forall b m0 m,
@@ -678,7 +678,7 @@ Proof.
                 learn (H1 _ H2)
               end; crush).
 Qed.
-Hint Resolve expr_runp_determinate : verilog.
+#[export] Hint Resolve expr_runp_determinate : verilog.
 
 Lemma location_is_determinate :
   forall f asr asa e l,
@@ -727,7 +727,7 @@ Lemma stmnt_runp_determinate :
                learn (H1 _ _ H2)
               end; crush).
 Qed.
-Hint Resolve stmnt_runp_determinate : verilog.
+#[export] Hint Resolve stmnt_runp_determinate : verilog.
 
 Lemma mi_stepp_determinate :
   forall f asr0 asa0 m asr1 asa1,
diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v
index b621632..d1494ec 100644
--- a/src/hls/Veriloggenproof.v
+++ b/src/hls/Veriloggenproof.v
@@ -115,7 +115,7 @@ Lemma Zle_relax :
   p < q <= r ->
   p <= q <= r.
 Proof. lia. Qed.
-Hint Resolve Zle_relax : verilogproof.
+#[local] Hint Resolve Zle_relax : verilogproof.
 
 Lemma transl_in :
   forall l p,
@@ -202,7 +202,7 @@ Proof.
     eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H.
     trivial. assumption.
 Qed.
-Hint Resolve transl_list_correct : verilogproof.
+#[local] Hint Resolve transl_list_correct : verilogproof.
 
 Lemma pc_wf :
   forall A m p v,
@@ -223,7 +223,7 @@ Proof.
   - intros. constructor.
   - intros. simplify. econstructor. constructor. auto.
 Qed.
-Hint Resolve mis_stepp_decl : verilogproof.
+#[local] Hint Resolve mis_stepp_decl : verilogproof.
 
 Lemma mis_stepp_negedge_decl :
   forall l asr asa f,
@@ -233,7 +233,7 @@ Proof.
   - intros. constructor.
   - intros. simplify. econstructor. constructor. auto.
 Qed.
-Hint Resolve mis_stepp_negedge_decl : verilogproof.
+#[local] Hint Resolve mis_stepp_negedge_decl : verilogproof.
 
 Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m.
 Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed.
@@ -348,7 +348,7 @@ Section CORRECTNESS.
   Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
   Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
-  Hint Resolve symbols_preserved : verilogproof.
+  #[local] Hint Resolve symbols_preserved : verilogproof.
 
   Lemma function_ptr_translated:
     forall (b: Values.block) (f: HTL.fundef),
@@ -359,7 +359,7 @@ Section CORRECTNESS.
     intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
-  Hint Resolve function_ptr_translated : verilogproof.
+  #[local] Hint Resolve function_ptr_translated : verilogproof.
 
   Lemma functions_translated:
     forall (v: Values.val) (f: HTL.fundef),
@@ -370,14 +370,14 @@ Section CORRECTNESS.
     intros. exploit (Genv.find_funct_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
-  Hint Resolve functions_translated : verilogproof.
+  #[local] Hint Resolve functions_translated : verilogproof.
 
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
   Proof.
     intros. eapply (Genv.senv_match TRANSL).
   Qed.
-  Hint Resolve senv_preserved : verilogproof.
+  #[local] Hint Resolve senv_preserved : verilogproof.
 
   Ltac unfold_replace :=
     match goal with
@@ -502,7 +502,7 @@ Section CORRECTNESS.
     - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial.
       repeat rewrite_eq. apply match_state. assumption.
   Qed.
-  Hint Resolve transl_step_correct : verilogproof.
+  #[local] Hint Resolve transl_step_correct : verilogproof.
 
   Lemma transl_initial_states :
     forall s1 : Smallstep.state (HTL.semantics prog),
@@ -520,7 +520,7 @@ Section CORRECTNESS.
     inv B. eauto.
     constructor.
   Qed.
-  Hint Resolve transl_initial_states : verilogproof.
+  #[local] Hint Resolve transl_initial_states : verilogproof.
 
   Lemma transl_final_states :
     forall (s1 : Smallstep.state (HTL.semantics prog))
@@ -532,7 +532,7 @@ Section CORRECTNESS.
   Proof.
     intros. inv H0. inv H. inv H3. constructor. reflexivity.
   Qed.
-  Hint Resolve transl_final_states : verilogproof.
+  #[local] Hint Resolve transl_final_states : verilogproof.
 
   Theorem transf_program_correct:
     forward_simulation (HTL.semantics prog) (Verilog.semantics tprog).