diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f1bd914854139..e187dcd68e3de 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2244,14 +2244,14 @@ as_or_and_ipat: [
 | "as" or_and_intropattern
 ]
 
-rewstrategy2: [
+rewstrategy1_list: [
 | DELETE rewstrategy1
-| REPLACE rewstrategy2 ";" rewstrategy1
+| REPLACE rewstrategy1_list ";" rewstrategy1
 | WITH LIST1 rewstrategy1 SEP ";"
 ]
 
 SPLICE: [
-| rewstrategy2
+| rewstrategy1_list
 | clause
 | noedit_mode
 | match_list
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index f213ac839011b..ff4ceaf6f9be2 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2279,11 +2279,11 @@ glob_constr_with_bindings: [
 
 rewstrategy: [
 | "fix" identref ":=" rewstrategy1
-| rewstrategy2
+| rewstrategy1_list
 ]
 
-rewstrategy2: [
-| rewstrategy2 ";" rewstrategy1
+rewstrategy1_list: [
+| rewstrategy1_list ";" rewstrategy1
 | rewstrategy1
 ]
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 80b2e83dc03fd..67c89ce8db9d4 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -66,8 +66,10 @@ END
 
 {
 
-(** XXX this seems incorrect? *)
-let subst_strategy s str = str
+let subst_strategy sub = map_strategy
+    (Tacsubst.subst_glob_constr_and_expr sub)
+    (Tacsubst.subst_redexp sub)
+    (fun x -> x)
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 let pr_raw_strategy env sigma prc prlc _ (s : Tacexpr.raw_strategy) =
@@ -97,9 +99,9 @@ GRAMMAR EXTEND Gram
   rewstrategy:
     [ NONA
       [ IDENT "fix"; id = identref; ":="; s = rewstrategy1 -> { StratFix (id, s) }
-      | h = rewstrategy2 -> { h } ] ]
+      | h = rewstrategy1_list -> { h } ] ]
   ;
-  rewstrategy2:
+  rewstrategy1_list:
     [ LEFTA
       [ h = SELF; ";"; h' = rewstrategy1 -> { StratBinary (Compose, h, h') }
       | h = rewstrategy1 -> { h } ] ]
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index b140cb53bf133..4a1ce76f66d61 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -760,16 +760,19 @@ let glob_tactic_env l env x =
 let intern_strategy ist s =
   let rec aux stratvars = function
     | Rewrite.StratVar x ->
+      (* We could make this whole branch assert false, since it's
+         unreachable except from plugins. But maybe it's useful if any
+         plug-in wants to craft a strategy by hand. *)
       if Id.Set.mem x.v stratvars then Rewrite.StratVar x.v
       else CErrors.user_err ?loc:x.loc Pp.(str "Unbound strategy" ++ spc() ++ Id.print x.v)
     | StratConstr ({ v = CRef (qid, None) }, true) when idset_mem_qualid qid stratvars ->
       let (_, x) = repr_qualid qid in Rewrite.StratVar x
+    | StratConstr (c, b) -> StratConstr (intern_constr ist c, b)
     | StratFix (x, s) -> StratFix (x.v, aux (Id.Set.add x.v stratvars) s)
     | StratId | StratFail | StratRefl as s -> s
     | StratUnary (s, str) -> StratUnary (s, aux stratvars str)
     | StratBinary (s, str, str') -> StratBinary (s, aux stratvars str, aux stratvars str')
     | StratNAry (s, strs) -> StratNAry (s, List.map (aux stratvars) strs)
-    | StratConstr (c, b) -> StratConstr (intern_constr ist c, b)
     | StratTerms l -> StratTerms (List.map (intern_constr ist) l)
     | StratHints (b, id) -> StratHints (b, id)
     | StratEval r -> StratEval (intern_red_expr ist r)
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c6d48a5cf2bda..ea6c7b337ae4a 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -31,3 +31,5 @@ val subst_glob_constr_and_expr :
 val subst_glob_with_bindings : substitution ->
   glob_constr_and_expr with_bindings ->
   glob_constr_and_expr with_bindings
+
+val subst_redexp : substitution -> Genredexpr.glob_red_expr -> Genredexpr.glob_red_expr
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
index 7720a07328519..bfb2a2527e8dd 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -54,6 +54,10 @@ val set_strategy :
 (** call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function
 
+(** [subst_red_expr sub c] performs the substitution [sub] on all kernel
+   names appearing in [c] *)
+val subst_red_expr : Mod_subst.substitution -> red_expr -> red_expr
+
 open Constrexpr
 open Libnames
 
diff --git a/test-suite/bugs/bug_18463.v b/test-suite/bugs/bug_18463.v
new file mode 100644
index 0000000000000..914554328d57f
--- /dev/null
+++ b/test-suite/bugs/bug_18463.v
@@ -0,0 +1,38 @@
+From Coq Require Import Setoid.
+
+Module Type Nop. End Nop.
+Module nop. End nop.
+
+Module RewriteStratSubstTestF (Nop : Nop).
+  Axiom X : Set.
+
+  Axiom f : X -> X.
+  Axiom g : X -> X -> X.
+  Axiom h : nat -> X -> X.
+
+  Axiom lem0 : forall x, f (f x) = f x.
+  Axiom lem1 : forall x, g x x = f x.
+  Axiom lem2 : forall n x, h (S n) x = g (h n x) (h n x).
+  Axiom lem3 : forall x, h 0 x = x.
+  Definition idnat := @id nat.
+
+  Ltac rs1 := rewrite_strat topdown lem2.
+  Ltac rs2 := rewrite_strat try fold idnat.
+  Ltac rs3 := rewrite_strat try subterms lem2.
+  Ltac rs4 := rewrite_strat eval cbv delta [idnat].
+End RewriteStratSubstTestF.
+
+Module RewriteStratSubstTest := RewriteStratSubstTestF nop.
+
+Goal forall x, RewriteStratSubstTest.h 6 x = RewriteStratSubstTest.f x /\ RewriteStratSubstTest.idnat 5 = id 5.
+  intros.
+  Print Ltac RewriteStratSubstTest.rs1. (* Ltac RewriteStratSubstTest.rs1 := Coq.Init.Ltac.rewrite_strat_#_521927FC _ (* Generic printer *) *)
+  RewriteStratSubstTest.rs1. (* Error: Anomaly "Constant rewrite_strat.RewriteStratSubstTestF.lem2 does not appear in the environment."
+Please report at http://coq.inria.fr/bugs/. *)
+Undo 1.
+  RewriteStratSubstTest.rs2.
+Undo 1.
+  RewriteStratSubstTest.rs3.
+Undo 1.
+  RewriteStratSubstTest.rs4.
+Admitted.