removing warnings on hints in core

11 files changed, 39 insertions, 42 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 02f9141b..bc9f2584 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1005,7 +1005,7 @@ Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi:
 Proof.
 
 (* a little tactic to automate reasoning on preg_eq *)
-Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr.
+Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
 Local Ltac preg_eq_discr r rd :=
   destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto);
   rewrite (assign_diff _ (#rd) (#r) _); auto;
@@ -1053,7 +1053,7 @@ Local Ltac preg_eq_discr r rd :=
         preg_eq_discr r rd0. }
 
     (* Load Octuple word *)
-    + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr.
+    + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
       unfold parexec_load_o_offset.
       destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl.
       rewrite H0, H.
@@ -1423,7 +1423,7 @@ Section SECT_BBLOCK_EQUIV.
 
 Variable Ge: genv.
 
-Local Hint Resolve trans_state_match.
+Local Hint Resolve trans_state_match: core.
 
 Lemma bblock_simu_reduce:
   forall p1 p2 ge fn,
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index ecb4629b..d3c2008f 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -859,7 +859,7 @@ Proof.
     destruct cmp; discriminate.
 Qed.
 
-Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct.
+Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core.
 
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m' tbb,
@@ -1163,7 +1163,7 @@ Proof.
   split; intros; Simpl.
 Qed.
 
-Local Hint Resolve Val_cmpu_correct Val_cmplu_correct.
+Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core.
 
 Lemma transl_condimm_int32u_correct:
   forall cmp rd r1 n k rs m,
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index fbb06c9b..3b123c75 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -567,7 +567,7 @@ Proof.
   unfold builtin_alone in H0. erewrite H0; eauto.
 Qed.
 
-Local Hint Resolve verified_schedule_nob_checks_alls_bundles.
+Local Hint Resolve verified_schedule_nob_checks_alls_bundles: core.
 
 Lemma verified_schedule_checks_alls_bundles bb lb bundle:
   verified_schedule bb = OK lb ->
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
index 5c94d435..cf46072f 100644
--- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
+++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v
@@ -403,7 +403,7 @@ Proof.
     * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto.
     * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto.
 Qed.
-Local Hint Resolve app_fail_allvalid_correct.
+Local Hint Resolve app_fail_allvalid_correct: core.
 
 Lemma app_fail_correct l pt t1 t2: 
   match_pt t1 pt -> 
diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v
index ea55b735..7a77ec15 100644
--- a/mppa_k1c/abstractbb/ImpSimuTest.v
+++ b/mppa_k1c/abstractbb/ImpSimuTest.v
@@ -304,12 +304,12 @@ Proof.
       rewrite <- EQT; eauto.
     + exploit smem_valid_set_decompose_1; eauto.
   - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
-    Local Hint Resolve smem_valid_set_decompose_1.
+    Local Hint Resolve smem_valid_set_decompose_1: core.
     intros; case (R.eq_dec x x0).
     + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
     + intros; rewrite !Dict.set_spec_diff; simpl; eauto.
 Qed.
-Local Hint Resolve naive_set_correct.
+Local Hint Resolve naive_set_correct: core.
 
 Definition equiv_hsmem ge (hd1 hd2: hsmem) := 
       (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m)
@@ -523,7 +523,7 @@ Lemma hinst_smem_correct i: forall hd hod,
   WHEN hinst_smem i hd hod ~> hd' THEN
     forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
 Proof.
-  Local Hint Resolve smem_valid_set_proof.
+  Local Hint Resolve smem_valid_set_proof: core.
   induction i; simpl; wlp_simplify; eauto 15 with wlp.
 Qed.
 Global Opaque hinst_smem.
@@ -563,7 +563,7 @@ Definition bblock_hsmem: bblock -> ?? hsmem
 Lemma bblock_hsmem_correct p:
   WHEN bblock_hsmem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd.
 Proof.
-  Local Hint Resolve hsmem_empty_correct.
+  Local Hint Resolve hsmem_empty_correct: core.
   wlp_simplify.
 Qed.
 Global Opaque bblock_hsmem.
@@ -775,7 +775,7 @@ Proof.
   intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid.
 Qed.
 
-Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv.
+Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv: core.
 
 Program Definition bblock_simu_test (p1 p2: bblock): ?? bool :=
   DO log <~ count_logger ();;
@@ -802,7 +802,7 @@ Obligation 2.
   wlp_simplify.
 Qed.
 
-Local Hint Resolve g_bblock_simu_test_correct.
+Local Hint Resolve g_bblock_simu_test_correct: core.
 
 Theorem bblock_simu_test_correct p1 p2:
   WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
@@ -1123,7 +1123,7 @@ Definition get {A} (d:t A) (x:R.t): option A
 Definition set {A} (d:t A) (x:R.t) (v:A): t A
  := PositiveMap.add x v d.
 
-Local Hint Unfold PositiveMap.E.eq.
+Local Hint Unfold PositiveMap.E.eq: core.
 
 Lemma set_spec_eq A d x (v: A):
   get (set d x v) x = Some v.
diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v
index d8002375..637116cc 100644
--- a/mppa_k1c/abstractbb/Impure/ImpHCons.v
+++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v
@@ -95,7 +95,7 @@ Proof.
   wlp_simplify.
 Qed.
 Global Opaque assert_list_incl.
-Hint Resolve assert_list_incl_correct.
+Hint Resolve assert_list_incl_correct: wlp.
 
 End Sets.
 
@@ -165,7 +165,7 @@ Lemma hConsV_correct A (hasheq: A -> A -> ?? bool):
     (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> 
     forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data).
 Proof.
-  Local Hint Resolve f_equal2.
+  Local Hint Resolve f_equal2: core.
   wlp_simplify.
   exploit H; eauto.
   + wlp_simplify.
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v
index 22809095..30904b5d 100644
--- a/mppa_k1c/abstractbb/Parallelizability.v
+++ b/mppa_k1c/abstractbb/Parallelizability.v
@@ -332,7 +332,7 @@ Fixpoint bblock_wframe(p:bblock): list R.t :=
   | i::p' => (inst_wframe i)++(bblock_wframe p') 
   end.
 
-Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm.
+Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_comm: core.
 
 Lemma bblock_wframe_Permutation p p': 
  Permutation p p' -> Permutation (bblock_wframe p)  (bblock_wframe p').
@@ -620,7 +620,7 @@ Include ParallelizablityChecking L.
 Section PARALLEL2.
 Variable ge: genv.
 
-Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame.
+Local Hint Resolve S.empty_match_frame S.add_match_frame S.union_match_frame S.is_disjoint_match_frame: core.
 
 (** Now, refinement of each operation toward parallelizable *)
 
@@ -659,14 +659,14 @@ Fixpoint inst_sframe (i: inst): S.t :=
   | a::i' => S.add (fst a) (S.union (exp_sframe (snd a)) (inst_sframe i'))
   end.
 
-Local Hint Resolve exp_sframe_correct.
+Local Hint Resolve exp_sframe_correct: core.
 
 Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
 Proof.
   induction i as [|[y e] i']; simpl; auto.
 Qed.
 
-Local Hint Resolve inst_wsframe_correct inst_sframe_correct.
+Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core.
 
 Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
   match p with
diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v
index 649dd083..e234883f 100644
--- a/mppa_k1c/abstractbb/SeqSimuTheory.v
+++ b/mppa_k1c/abstractbb/SeqSimuTheory.v
@@ -102,9 +102,6 @@ Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
      let d':=inst_smem i d d in
      bblock_smem_rec p' d'
   end.
-(*
-Local Hint Resolve smem_eval_empty.
-*)
 
 Definition bblock_smem: bblock -> smem
  := fun p => bblock_smem_rec p smem_empty.
@@ -124,7 +121,7 @@ Proof.
   intros d a H; eapply inst_smem_pre_monotonic; eauto.
 Qed.
 
-Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic.
+Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic: core.
 
 Lemma term_eval_exp e (od:smem) m0 old:
   (forall x, term_eval ge (od x) m0 = Some (old x)) ->
@@ -185,7 +182,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem),
   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
   forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
 Proof.
-  Local Hint Resolve inst_smem_Some_correct1.
+  Local Hint Resolve inst_smem_Some_correct1: core.
   induction p as [ | i p]; simpl; intros m1 m2 d H.
   - inversion_clear H; eauto.
   - intros H0 x0.
@@ -299,7 +296,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem),
   (forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
   pre (bblock_smem_rec p d) ge m0.
 Proof.
-  Local Hint Resolve inst_valid.
+  Local Hint Resolve inst_valid: core.
   induction p as [ | i p]; simpl; intros m1 d H; auto.
   intros H0 H1.
   destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
@@ -326,7 +323,7 @@ Theorem bblock_smem_simu p1 p2:
    smem_simu (bblock_smem p1) (bblock_smem p2) ->
    bblock_simu ge p1 p2.
 Proof.
-  Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1.
+  Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core.
   intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
   destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence.
   assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 940c6563..58455ada 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -414,7 +414,7 @@ Proof.
 Qed.
 
 
-Local Hint Resolve code_tail_0 code_tail_S.
+Local Hint Resolve code_tail_0 code_tail_S: core.
 
 Lemma code_tail_next:
   forall fn ofs c0,
@@ -458,7 +458,7 @@ Proof.
   omega.
 Qed.
 
-Local Hint Resolve code_tail_next.
+Local Hint Resolve code_tail_next: core.
 
 Lemma code_tail_next_int:
   forall fn ofs bi c,
diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v
index 39dd2234..224eda0a 100644
--- a/mppa_k1c/lib/ForwardSimulationBlock.v
+++ b/mppa_k1c/lib/ForwardSimulationBlock.v
@@ -21,7 +21,7 @@ Section starN_lemma.
 
 Variable L: semantics.
 
-Local Hint Resolve starN_refl starN_step Eapp_assoc.
+Local Hint Resolve starN_refl starN_step Eapp_assoc: core.
 
 Lemma starN_split n s t s':
   starN (step L) (globalenv L) n s t s' ->
@@ -93,7 +93,7 @@ Hypothesis simu_end_block:
 
 (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *)
 
-Local Hint Resolve starN_refl starN_step.
+Local Hint Resolve starN_refl starN_step: core.
 
 Definition follows_in_block (head current: state L1): Prop :=
   dist_end_block head >= dist_end_block current 
@@ -164,7 +164,7 @@ Inductive is_well_memorized (s s': memostate): Prop :=
     memorized s' = None ->
     is_well_memorized s s'.
 
-Local Hint Resolve StartBloc MidBloc ExitBloc.
+Local Hint Resolve StartBloc MidBloc ExitBloc: core.
 
 Definition memoL1 := {| 
   state := memostate;
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v
index 91be5e2e..0de2df52 100644
--- a/mppa_k1c/lib/Machblockgenproof.v
+++ b/mppa_k1c/lib/Machblockgenproof.v
@@ -72,7 +72,7 @@ Proof.
   apply match_states_trans_state.
 Qed.
 
-Local Hint Resolve match_states_trans_state.
+Local Hint Resolve match_states_trans_state: core.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -284,7 +284,7 @@ Proof.
 Qed.
 
 Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated
-                   parent_sp_preserved.
+                   parent_sp_preserved: core.
 
 
 Definition dist_end_block_code (c: Mach.code) := 
@@ -299,8 +299,8 @@ Definition dist_end_block (s: Mach.state): nat :=
   | _ => 0
   end.
 
-Local Hint Resolve exec_nil_body exec_cons_body.
-Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore.
+Local Hint Resolve exec_nil_body exec_cons_body: core.
+Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core.
 
 Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
 Proof.
@@ -336,7 +336,7 @@ Proof.
     omega.
 Qed.
 
-Local Hint Resolve dist_end_block_code_simu_mid_block.
+Local Hint Resolve dist_end_block_code_simu_mid_block: core.
 
 
 Lemma size_nonzero c b bl:
@@ -392,8 +392,8 @@ destruct i; congruence.
 Qed.
 
 
-Local Hint Resolve Mlabel_is_not_cfi.
-Local Hint Resolve MBbasic_is_not_cfi.
+Local Hint Resolve Mlabel_is_not_cfi: core.
+Local Hint Resolve MBbasic_is_not_cfi: core.
 
 Lemma add_to_new_block_is_label i:
   header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l.
@@ -408,7 +408,7 @@ Proof.
   + unfold cfi_bblock in H; simpl in H; congruence.
 Qed.
 
-Local Hint Resolve Mlabel_is_not_basic.
+Local Hint Resolve Mlabel_is_not_basic: core.
 
 Lemma trans_code_decompose c: forall b bl,
   is_trans_code c (b::bl) ->
@@ -510,8 +510,8 @@ Proof.
     rewrite Hs2, Hb2; eauto.
     Qed. 
 
-Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit.
-Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same.
+Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit: core.
+Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core.
 
 
 Lemma match_states_concat_trans_code st f sp c rs m h: