Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

5 files changed, 17 insertions, 14 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index dbfe5e5d..dc25b516 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -161,7 +161,9 @@ let builtins_generic = {
       @
     [
     (* Integer arithmetic *)
-    "__builtin_bswap",
+    "__builtin_bswap64",
+    (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
+      "__builtin_bswap",
     (TInt(IUInt, []), [TInt(IUInt, [])], false);
     "__builtin_bswap32",
       (TInt(IUInt, []), [TInt(IUInt, [])], false);
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 *)