4 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index a618fc781f..3a7cf41d43 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr.
 Lemma is_true_true : true.               Proof. by []. Qed.
 Lemma not_false_is_true : ~ false.       Proof. by []. Qed.
 Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
-Hint Resolve is_true_true not_false_is_true is_true_locked_true.
+Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
 
 (**  Shorter names.  **)
 Definition isT := is_true_true.
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 648bb00d5c..fa58a1c39a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -859,7 +859,7 @@ let ssr_n_tac seed n gl =
     with Not_found ->
       if n = -1 then fail "The ssreflect library was not loaded"
       else fail ("The tactic "^name^" was not found") in
-  let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+  let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
   Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl
 
 let donetac n gl = ssr_n_tac "done" n gl
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index e2c0ed7c8b..6535cad8b7 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -398,7 +398,7 @@ End ExtensionalEquality.
 Typeclasses Opaque eqfun.
 Typeclasses Opaque eqrel.
 
-Hint Resolve frefl rrefl.
+Hint Resolve frefl rrefl : core.
 
 Notation "f1 =1 f2" := (eqfun f1 f2)
   (at level 70, no associativity) : fun_scope.
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 52240f5896..7c91860228 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1545,9 +1545,9 @@ let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
 let swaptacarg (loc, b) = (b, []), Some (TacId [])
 
 let check_seqtacarg dir arg = match snd arg, dir with
-  | ((true, []), Some (TacAtom (loc, _))), L2R ->
+  | ((true, []), Some (TacAtom { CAst.loc })), L2R ->
     CErrors.user_err ?loc (str "expected \"last\"")
-  | ((false, []), Some (TacAtom (loc, _))), R2L ->
+  | ((false, []), Some (TacAtom { CAst.loc })), R2L ->
     CErrors.user_err ?loc (str "expected \"first\"")
   | _, _ -> arg
 
@@ -1677,7 +1677,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
     | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
   let tacname = ssrtac_name name in () *)
 
-let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args))
+let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args))
 let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args
 
 let tclintros_expr ?loc tac ipats =
@@ -1704,7 +1704,7 @@ END
 
 GRAMMAR EXTEND Gram
   GLOBAL: tactic_expr;
-  ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]];
+  ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
   tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]];
 END
 
@@ -1724,7 +1724,7 @@ let ssrautoprop gl =
     let tacname = 
       try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop"))
       with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in
-    let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
+    let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in
     V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl
   with Not_found -> V82.of_tactic (Auto.full_trivial []) gl