diff --git a/Makefile.local.common b/Makefile.local.common
index 713a49b9d..e4523a625 100644
--- a/Makefile.local.common
+++ b/Makefile.local.common
@@ -23,8 +23,13 @@ ifneq (,$(filter 8.16%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v816
 ML_DESCRIPTION := "Coq v8.16"
 else
+ifneq (,$(filter 8.17%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v817
 ML_DESCRIPTION := "Coq v8.17"
+else
+EXPECTED_EXT:=.v818
+ML_DESCRIPTION := "Coq v8.18"
+endif
 endif
 endif
 
diff --git a/src/Rewriter/Util/plugins/Ltac2Extra.v.v818 b/src/Rewriter/Util/plugins/Ltac2Extra.v.v818
new file mode 100644
index 000000000..047dea5b7
--- /dev/null
+++ b/src/Rewriter/Util/plugins/Ltac2Extra.v.v818
@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "coq-rewriter.ltac2_extra".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "coq-rewriter.ltac2_extra" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.
diff --git a/src/Rewriter/Util/plugins/RewriterBuild.v.v818 b/src/Rewriter/Util/plugins/RewriterBuild.v.v818
new file mode 100644
index 000000000..7edae6c56
--- /dev/null
+++ b/src/Rewriter/Util/plugins/RewriterBuild.v.v818
@@ -0,0 +1,10 @@
+Require Import Rewriter.Util.plugins.RewriterBuildRegistry.
+
+Declare ML Module "coq-rewriter.rewriter_build".
+
+Ltac Rewrite_lhs_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_lhs_for verified_rewriter_package.
+Ltac Rewrite_rhs_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_rhs_for verified_rewriter_package.
+Ltac Rewrite_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_for verified_rewriter_package.
+
+Export Pre.RewriteRuleNotations.
+Export IdentifiersGenerateProofs.Compilers.pattern.ProofTactic.Settings.
diff --git a/src/Rewriter/Util/plugins/RewriterBuildRegistry.v.v818 b/src/Rewriter/Util/plugins/RewriterBuildRegistry.v.v818
new file mode 100644
index 000000000..605f5ede4
--- /dev/null
+++ b/src/Rewriter/Util/plugins/RewriterBuildRegistry.v.v818
@@ -0,0 +1,20 @@
+Require Export Rewriter.Util.plugins.RewriterBuildRegistryImports.
+
+Register Basic.GoalType.package_with_args as rewriter.basic_package_with_args.type.
+Register Basic.GoalType.base_elim_with_args as rewriter.base_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.ident_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.pattern_ident_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.raw_ident_elim_with_args.type.
+Register ScrapedData.t_with_args as rewriter.scraped_data_with_args.type.
+Register rules_proofsT_with_args as rewriter.rules_proofs_with_args.type.
+Register InductiveHList.nil as rewriter.ident_list.nil.
+Register RewriteRules.GoalType.VerifiedRewriter_with_ind_args as rewriter.verified_rewriter_with_args.type.
+
+Ltac make_base_elim_with_args := Basic.PrintBase.make_base_elim.
+Ltac make_ident_elim_with_args := Basic.PrintIdent.make_ident_elim.
+Ltac make_pattern_ident_elim_with_args := Basic.PrintIdent.make_pattern_ident_elim.
+Ltac make_raw_ident_elim_with_args := Basic.PrintIdent.make_raw_ident_elim.
+Ltac make_basic_package_with_args := Basic.Tactic.make_package.
+Ltac make_scraped_data_with_args := Basic.ScrapeTactics.make_scrape_data.
+Ltac make_verified_rewriter_with_args := RewriteRules.Tactic.make_rewriter_all.
+Ltac make_rules_proofs_with_args := Basic.ScrapeTactics.make_rules_proofsT_with_args.
diff --git a/src/Rewriter/Util/plugins/StrategyTactic.v.v818 b/src/Rewriter/Util/plugins/StrategyTactic.v.v818
new file mode 100644
index 000000000..53419cad5
--- /dev/null
+++ b/src/Rewriter/Util/plugins/StrategyTactic.v.v818
@@ -0,0 +1,35 @@
+Declare ML Module "coq-rewriter.strategy_tactic".
+
+(*
+(* TEST: *)
+
+Definition id0 {A} (x : A) := x.
+Definition id1 {A} (x : A) := x.
+Definition id2 {A} (x : A) := id1 x.
+Definition id3 {A} (x : A) := id1 x.
+Definition id4 := id1 O.
+
+(* Works locally *)
+Goal exists x : nat, id0 x = id4.
+Proof.
+  strategy 1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 O) end.
+  Undo.
+  strategy -1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+  reflexivity.
+Abort.
+
+(* works globally *)
+Goal exists x : nat, id0 x = id4.
+Proof.
+  strategy -1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+  reflexivity.
+Defined.
+
+Goal exists x : nat, id0 x = id4.
+Proof.
+  eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+Abort.
+*)
diff --git a/src/Rewriter/Util/plugins/definition_by_tactic.ml.v818 b/src/Rewriter/Util/plugins/definition_by_tactic.ml.v818
new file mode 100644
index 000000000..e89bcba4d
--- /dev/null
+++ b/src/Rewriter/Util/plugins/definition_by_tactic.ml.v818
@@ -0,0 +1,17 @@
+open Ltac_plugin
+
+let make_definition_by_tactic sigma ~poly (name : Names.Id.t) (ty : EConstr.t) (tac : unit Proofview.tactic) =
+  let cinfo = Declare.CInfo.make ~name ~typ:ty () in
+  let info = Declare.Info.make ~poly () in
+  let lemma = Declare.Proof.start ~cinfo ~info sigma in
+  let lemma, _ = Declare.Proof.by tac lemma in
+  let ids = Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in
+  match ids with
+  | [Names.GlobRef.ConstRef cst] -> cst
+  | _ -> CErrors.user_err (Pp.str "Internal error in make_definition_by_tactic")
+
+let vernac_make_definition_by_tactic ~poly (name : Names.Id.t) (ty : Constrexpr.constr_expr) tac =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, ty) = Constrintern.interp_constr_evars env sigma ty in
+  ignore(make_definition_by_tactic sigma ~poly name ty (Tacinterp.interp tac))
diff --git a/src/Rewriter/Util/plugins/definition_by_tactic.mli.v818 b/src/Rewriter/Util/plugins/definition_by_tactic.mli.v818
new file mode 100644
index 000000000..36a07dfb9
--- /dev/null
+++ b/src/Rewriter/Util/plugins/definition_by_tactic.mli.v818
@@ -0,0 +1,11 @@
+open Ltac_plugin
+
+val make_definition_by_tactic
+  : Evd.evar_map
+  -> poly:bool
+  -> Names.Id.t
+  -> EConstr.t
+  -> unit Proofview.tactic
+  -> Names.Constant.t
+
+val vernac_make_definition_by_tactic : poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Tacexpr.raw_tactic_expr -> unit
diff --git a/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v818 b/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v818
new file mode 100644
index 000000000..f3cbbd704
--- /dev/null
+++ b/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v818
@@ -0,0 +1,22 @@
+{
+
+open Stdarg
+open Ltac_plugin
+open Tacarg
+open Definition_by_tactic
+
+}
+
+DECLARE PLUGIN "coq-rewriter.definition_by_tactic"
+
+VERNAC COMMAND EXTEND DefinitionViaTactic CLASSIFIED AS SIDEFF
+  | [ "Make" "Definition" ":" constr(ty) ":=" tactic(tac) ] -> {
+    let poly = false in
+    let name = Namegen.next_global_ident_away (Names.Id.of_string "Unnamed_thm") Names.Id.Set.empty in
+    vernac_make_definition_by_tactic ~poly name ty tac
+  }
+  | [ "Make" "Definition" ident(name) ":" constr(ty) ":=" tactic(tac) ] -> {
+    let poly = false in
+    vernac_make_definition_by_tactic ~poly name ty tac
+  }
+END
diff --git a/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib.v818 b/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib.v818
new file mode 100644
index 000000000..029c03128
--- /dev/null
+++ b/src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib.v818
@@ -0,0 +1,2 @@
+Definition_by_tactic
+Definition_by_tactic_plugin
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.ml.v818 b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v818
new file mode 100644
index 000000000..9a31cfa14
--- /dev/null
+++ b/src/Rewriter/Util/plugins/inductive_from_elim.ml.v818
@@ -0,0 +1,82 @@
+open Constr
+open Genredexpr
+open Names
+open Context
+open Entries
+
+let rec make_constructor_types env sigma (avoid : Id.Set.t) (body : EConstr.t) =
+  match EConstr.kind sigma body with
+  | Prod (cname, cty, body) ->
+    if EConstr.Vars.noccurn sigma 1 body
+    then (* the rest does not depend on this term, so we treat it as a constructor *)
+      (* We pass the empty set on the inner next_name because we care about avoiding other constructor names, which we treat as extra global identifiers *)
+      let cname = Namegen.next_global_ident_away (Namegen.next_name_away cname.binder_name Id.Set.empty) avoid in
+      let avoid = Id.Set.add cname avoid in
+      let dummy_arg = EConstr.mkProp in
+      let (sigma, avoid, rest_ctors) = make_constructor_types env sigma avoid (EConstr.Vars.subst1 dummy_arg body) in
+      (sigma, avoid, (cname, cty) :: rest_ctors)
+    else
+      (* the rest does depend on this argument, so we treat it as part of the final conclusion, and consider ourselves done *)
+      (sigma, avoid, [])
+  | Var _ ->
+    (* we are at the end of the inductive chain *)
+    (sigma, avoid, [])
+  | _ ->
+    CErrors.user_err Pp.(str "Invalid non-arrow component of eliminator type:" ++ Printer.pr_econstr_env env sigma body)
+
+let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr.t) =
+  let env = Global.env () in
+  let (hnffun, _) = Redexpr.reduction_of_red_expr env Hnf in
+  let (sigma, elim_ty) = hnffun env sigma elim_ty in
+  match EConstr.kind sigma elim_ty with
+  | Prod (ind_name, ind_ty, body) ->
+    (* If the user gives a name explicitly, we use exactly that name;
+       if the user gives a name via a binder name, we are more fuzzy
+       and search for the next free global identifier *)
+    let name = match name with
+      | Some name -> name
+      | None -> Namegen.next_global_ident_away (Namegen.next_name_away ind_name.binder_name Id.Set.empty) Id.Set.empty
+    in
+    let body = EConstr.Vars.subst1 (EConstr.mkVar name) body in
+    let (sigma, _, ctor_types) = make_constructor_types env sigma (Id.Set.singleton name) body in
+    let ctor_type_to_constr cty =
+      EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
+    in
+    let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
+    let uctx = match univs with
+    | UState.Monomorphic_entry ctx ->
+      let () = DeclareUctx.declare_universe_context ~poly:false ctx in
+      Entries.Monomorphic_ind_entry
+    | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
+    in
+    let mie = {
+      mind_entry_record = None;
+      mind_entry_finite = Declarations.Finite;
+      mind_entry_params = [];
+      mind_entry_inds = [{
+          mind_entry_typename = name;
+          mind_entry_arity = EConstr.to_constr sigma ind_ty;
+          mind_entry_consnames = List.map (fun (cname, cty) -> cname) ctor_types;
+          mind_entry_lc = List.map (fun (cname, cty) -> ctor_type_to_constr cty) ctor_types
+        }];
+      mind_entry_universes = uctx;
+      mind_entry_variance = None;
+      mind_entry_private = None;
+    } in
+    let sigma =
+      let uctx = Evd.evar_universe_context sigma in
+      let uctx = UState.demote_seff_univs (fst (Evd.universe_context_set sigma)) uctx in
+      Evd.set_universe_context sigma uctx
+    in
+    (sigma,
+     (DeclareInd.declare_mutual_inductive_with_eliminations
+        mie (univs, UnivNames.empty_binders) [([], List.map (fun _ -> []) ctor_types)],
+      0))
+  | _ ->
+    CErrors.user_err Pp.(str "Invalid non-arrow eliminator type:" ++ Printer.pr_econstr_env env sigma elim_ty)
+
+let vernac_make_inductive_from_elim name elim_ty =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, elim_ty) = Constrintern.interp_constr_evars env sigma elim_ty in
+  ignore(make_inductive_from_elim sigma name elim_ty)
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim.mli.v818 b/src/Rewriter/Util/plugins/inductive_from_elim.mli.v818
new file mode 100644
index 000000000..799c215f2
--- /dev/null
+++ b/src/Rewriter/Util/plugins/inductive_from_elim.mli.v818
@@ -0,0 +1,3 @@
+val make_inductive_from_elim : Evd.evar_map -> Names.Id.t option -> EConstr.t -> Evd.evar_map * Names.inductive
+
+val vernac_make_inductive_from_elim : Names.Id.t option -> Constrexpr.constr_expr -> unit
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg.v818 b/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg.v818
new file mode 100644
index 000000000..07f6b00cd
--- /dev/null
+++ b/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg.v818
@@ -0,0 +1,17 @@
+{
+
+open Stdarg
+open Inductive_from_elim
+
+}
+
+DECLARE PLUGIN "coq-rewriter.inductive_from_elim"
+
+VERNAC COMMAND EXTEND InductiveViaElim CLASSIFIED AS SIDEFF
+  | [ "Make" "Inductive" "From" "Elim" "Type" constr(elim_ty) ] -> {
+    vernac_make_inductive_from_elim None elim_ty
+  }
+  | [ "Make" ident(name) ":=" "Inductive" "From" "Elim" "Type" constr(elim_ty) ] -> {
+    vernac_make_inductive_from_elim (Some name) elim_ty
+  }
+END
diff --git a/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib.v818 b/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib.v818
new file mode 100644
index 000000000..126cdcdf8
--- /dev/null
+++ b/src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib.v818
@@ -0,0 +1,2 @@
+Inductive_from_elim
+Inductive_from_elim_plugin
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.ml.v818 b/src/Rewriter/Util/plugins/ltac2_extra.ml.v818
new file mode 100644
index 000000000..38e6b123d
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra.ml.v818
@@ -0,0 +1,19 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Proofview.Notations
+
+let pname s = { mltac_plugin = "coq-rewriter.ltac2_extra"; mltac_tactic = s }
+
+let define_primitive name arity f =
+  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure arity f)
+
+let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
+  f (Tac2ffi.repr_to r0 x) (Tac2ffi.repr_to r1 y)
+end
+
+let () = define2 "constr_equal_nounivs" constr constr begin fun c1 c2 ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr_nounivs sigma c1 c2 in
+  Proofview.tclUNIT (Tac2ffi.of_bool b)
+end
diff --git a/src/Rewriter/Util/plugins/ltac2_extra.mli.v818 b/src/Rewriter/Util/plugins/ltac2_extra.mli.v818
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v818 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v818
new file mode 100644
index 000000000..caffbc0a6
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v818
@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"
diff --git a/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v818 b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v818
new file mode 100644
index 000000000..c1effb855
--- /dev/null
+++ b/src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v818
@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin
diff --git a/src/Rewriter/Util/plugins/rewriter_build.ml.v818 b/src/Rewriter/Util/plugins/rewriter_build.ml.v818
new file mode 100644
index 000000000..126c31da1
--- /dev/null
+++ b/src/Rewriter/Util/plugins/rewriter_build.ml.v818
@@ -0,0 +1,196 @@
+open Ltac_plugin
+open Tacexpr
+open Constr
+open EConstr
+open Genredexpr
+open Names
+open Locus
+open Inductive_from_elim
+open Definition_by_tactic
+
+
+(*let r_scraped_data_ty () = Coqlib.lib_ref "rewriter.scraped_data.type"*)
+let r_scraped_data_with_args () = Coqlib.lib_ref "rewriter.scraped_data_with_args.type"
+let r_base_elim_with_args () = Coqlib.lib_ref "rewriter.base_elim_with_args.type"
+let r_ident_elim_with_args () = Coqlib.lib_ref "rewriter.ident_elim_with_args.type"
+let r_pattern_ident_elim_with_args () = Coqlib.lib_ref "rewriter.pattern_ident_elim_with_args.type"
+let r_raw_ident_elim_with_args () = Coqlib.lib_ref "rewriter.raw_ident_elim_with_args.type"
+let r_verified_rewriter_with_args () = Coqlib.lib_ref "rewriter.verified_rewriter_with_args.type"
+let r_ident_list_nil () = Coqlib.lib_ref "rewriter.ident_list.nil"
+let r_rules_proofs_with_args () = Coqlib.lib_ref "rewriter.rules_proofs_with_args.type"
+let r_true () = Coqlib.lib_ref "core.bool.true"
+let r_false () = Coqlib.lib_ref "core.bool.false"
+
+let rewriter_path =
+  DirPath.make (List.map Id.of_string ["RewriterBuildRegistry";"plugins";"Util";"Rewriter"])
+
+(* taken from https://github.com/coq/coq/blob/b6dcb301a1a34df8e4586e8cde6618e7c895fa08/plugins/setoid_ring/newring.ml#L161-L163 *)
+(* Calling a global tactic *)
+let ltac_call tac (args:glob_tactic_arg list) =
+  CAst.make @@ TacArg(TacCall (CAst.make (ArgArg(Loc.tag @@ tac),args)))
+
+let tactic_of_name (name : string) : unit Proofview.tactic =
+  try
+    Tacinterp.eval_tactic (ltac_call (KerName.make (ModPath.MPfile rewriter_path) (Label.make name)) [])
+  with Not_found -> CErrors.user_err Pp.(str "Not_found while trying to eval tactic " ++ str name)
+
+let base_elim_with_args_tac = tactic_of_name "make_base_elim_with_args"
+let ident_elim_with_args_tac = tactic_of_name "make_ident_elim_with_args"
+let pattern_ident_elim_with_args_tac = tactic_of_name "make_pattern_ident_elim_with_args"
+let raw_ident_elim_with_args_tac = tactic_of_name "make_raw_ident_elim_with_args"
+let scraped_data_with_args_tac = tactic_of_name "make_scraped_data_with_args"
+let verified_rewriter_with_args_tac = tactic_of_name "make_verified_rewriter_with_args"
+let rules_proofs_with_args_tac = tactic_of_name "make_rules_proofs_with_args"
+
+let name_or name default_name =
+  match name with
+  | Some name -> name
+  | None -> Namegen.next_global_ident_away (Names.Id.of_string default_name) Id.Set.empty
+
+let rec projT2_skip_cast env sigma c =
+  match EConstr.kind sigma c with
+  | Cast (c, _, _) -> projT2_skip_cast env sigma c
+  | App (_existT, [|_tA; _tP; _proj1; proj2|]) -> proj2
+  | App (_, args) ->
+    CErrors.user_err Pp.(str "Not an existT: Incorrect number of arguments (" ++ int (Array.length args) ++ str "): " ++ Printer.pr_econstr_env env sigma c)
+  | _ -> CErrors.user_err Pp.(str "Not an existT: " ++ Printer.pr_econstr_env env sigma c)
+
+
+let rewriter_heuristic_process_rules_proofs env sigma ~poly rules_proofs =
+  let (sigma, rules_proofs_ty) = Typing.type_of env sigma rules_proofs in
+  let (sigma, rules_proofs_with_args) = Evd.fresh_global env sigma (r_rules_proofs_with_args ()) in
+  let rules_proofs_with_args = mkApp (rules_proofs_with_args, [|rules_proofs_ty; rules_proofs|]) in
+  let uctx = Evd.evar_universe_context sigma in
+  let (rules_proofs_sig, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:rules_proofs_with_args rules_proofs_with_args_tac in
+  let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
+  let rules_proofs_sig = EConstr.of_constr rules_proofs_sig in
+  (sigma, projT2_skip_cast env sigma rules_proofs_sig)
+
+let rules_ty_of_rules_proofs env sigma rules_proofs =
+  let (sigma, rules_proofs_ty) = Typing.type_of env sigma rules_proofs in
+  match EConstr.kind sigma rules_proofs_ty with
+  | App (_hlist, [|_A; _snd; rules_ty|]) -> rules_ty
+  | App (_, args)
+    -> CErrors.user_err Pp.(str "Invalid type for rules_proofs: Incorrect number of arguments (" ++ int (Array.length args) ++ str "): " ++ Printer.pr_econstr_env env sigma rules_proofs_ty)
+  | _ -> CErrors.user_err Pp.(str "Invalid type for rules_proofs: " ++ Printer.pr_econstr_env env sigma rules_proofs_ty)
+
+
+let rewriter_scrape_data env sigma ~poly (rules_proofs : EConstr.t) (extra : EConstr.t) =
+  let (sigma, scraped_data_with_args) = Evd.fresh_global env sigma (r_scraped_data_with_args ()) in
+  let rules_ty = rules_ty_of_rules_proofs env sigma rules_proofs in
+  let (sigma, extra_ty) = Typing.type_of env sigma extra in
+  let scraped_data_ty = mkApp (scraped_data_with_args, [|rules_ty; rules_proofs; extra_ty; extra|]) in
+  let uctx = Evd.evar_universe_context sigma in
+  let (scraped_data, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:scraped_data_ty scraped_data_with_args_tac in
+  let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
+  (sigma, EConstr.of_constr scraped_data)
+
+let rewriter_emit_inductives sigma ~poly (scraped_data : EConstr.t) (base_name : Names.Id.t option) (ident_name : Names.Id.t option) (raw_ident_name : Names.Id.t option) (pattern_ident_name : Names.Id.t option) =
+  let env = Global.env () in
+  let (hnffun, _) = Redexpr.reduction_of_red_expr env Hnf in
+  let (sigma, scraped_data) = hnffun env sigma scraped_data in
+  let (sigma, base_elim_with_args) = Evd.fresh_global env sigma (r_base_elim_with_args ()) in
+  let base_elim_ty = mkApp (base_elim_with_args, [|scraped_data|]) in
+  let (sigma, ident_elim_with_args) = Evd.fresh_global env sigma (r_ident_elim_with_args ()) in
+  let (sigma, pattern_ident_elim_with_args) = Evd.fresh_global env sigma (r_pattern_ident_elim_with_args ()) in
+  let (sigma, raw_ident_elim_with_args) = Evd.fresh_global env sigma (r_raw_ident_elim_with_args ()) in
+  let uctx = Evd.evar_universe_context sigma in
+  let (base_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:base_elim_ty base_elim_with_args_tac in
+  let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
+  let base_name = name_or base_name "base" in
+  let (sigma, base) = make_inductive_from_elim sigma (Some base_name) (EConstr.of_constr base_elim) in
+  let base = mkInd base in
+  let ident_elim_ty = mkApp (ident_elim_with_args, [|scraped_data;base|]) in
+  let pattern_ident_elim_ty = mkApp (pattern_ident_elim_with_args, [|scraped_data;base|]) in
+  let raw_ident_elim_ty = mkApp (raw_ident_elim_with_args, [|scraped_data;base|]) in
+  let uctx = Evd.evar_universe_context sigma in
+  let (ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:ident_elim_ty ident_elim_with_args_tac in
+  let (pattern_ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:pattern_ident_elim_ty pattern_ident_elim_with_args_tac in
+  let (raw_ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
+    Declare.build_by_tactic env ~uctx ~poly ~typ:raw_ident_elim_ty raw_ident_elim_with_args_tac in
+  let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
+  let ident_name = name_or ident_name "ident" in
+  let (sigma, ident) = make_inductive_from_elim sigma (Some ident_name) (EConstr.of_constr ident_elim) in
+  let pattern_ident_name = name_or pattern_ident_name "pattern_ident" in
+  let (sigma, pattern_ident) = make_inductive_from_elim sigma (Some pattern_ident_name) (EConstr.of_constr pattern_ident_elim) in
+  let raw_ident_name = name_or raw_ident_name "raw_ident" in
+  let (sigma, raw_ident) = make_inductive_from_elim sigma (Some raw_ident_name) (EConstr.of_constr raw_ident_elim) in
+  (sigma, (base, mkInd ident, mkInd raw_ident, mkInd pattern_ident))
+
+let head sigma c =
+  match EConstr.kind sigma c with
+  | App (f, _) -> f
+  | _ -> c
+
+let set_strategy_of_package sigma level verified_rewriter_package =
+  let env = Global.env () in
+  let (hnffun, _) = Redexpr.reduction_of_red_expr env Hnf in
+  let (sigma, verified_rewriter_package) = hnffun env sigma verified_rewriter_package in
+  let exprInfo = match EConstr.kind sigma verified_rewriter_package with
+    | App (_build, args) -> args.(0)
+    | _ -> CErrors.user_err Pp.(str "Invalid hnf of verified rewriter package: " ++ Printer.pr_econstr_env env sigma verified_rewriter_package)
+  in
+  match EConstr.kind sigma exprInfo with
+  | App (_build, [|base; ident; base_interp; ident_interp|]) ->
+    let local = false in
+    let evaluable_head v = Tacred.evaluable_of_global_reference env (Patternops.head_of_constr_reference sigma (head sigma v)) in
+    Redexpr.set_strategy local
+      [(Conv_oracle.Level level,
+        List.map evaluable_head [base_interp; ident_interp])];
+    sigma
+  | App (_, args) ->
+    CErrors.user_err Pp.(str "Invalid hnf of exprInfo: Incorrect number of arguments (" ++ int (Array.length args) ++ str "): " ++ Printer.pr_econstr_env env sigma exprInfo)
+  | _ ->
+    CErrors.user_err Pp.(str "Invalid hnf of exprInfo: " ++ Printer.pr_econstr_env env sigma exprInfo)
+
+let make_rewriter_of_scraped_and_ind sigma ~poly package_name scraped_data var_like_idents base ident raw_ident pattern_ident include_interp skip_early_reduction skip_early_reduction_no_dtree rules_proofs =
+  let env = Global.env () in
+  let (sigma, verified_rewriter_with_args) = Evd.fresh_global env sigma (r_verified_rewriter_with_args ()) in
+  let rules_ty = rules_ty_of_rules_proofs env sigma rules_proofs in
+  let verified_rewriter_ty = mkApp (verified_rewriter_with_args, [|scraped_data; var_like_idents; base; ident; raw_ident; pattern_ident; include_interp; skip_early_reduction; skip_early_reduction_no_dtree; rules_ty; rules_proofs|]) in
+  (* force a typecheck of the application, propogate universe constraints *)
+  let (sigma, _) = Typing.type_of env sigma verified_rewriter_ty in
+  (* add universe constraints to the global env *)
+  let _ = Evd.univ_entry ~poly sigma in
+  let verified_rewriter_name = make_definition_by_tactic sigma ~poly package_name verified_rewriter_ty verified_rewriter_with_args_tac in
+  let sigma = Evd.from_env (Global.env ()) in
+  let verified_rewriter = mkConst verified_rewriter_name in
+  let sigma = set_strategy_of_package sigma (-1000) verified_rewriter in
+  (sigma, verified_rewriter)
+
+let make_rewriter sigma ~poly ~var_like_idents ~include_interp ~skip_early_reduction ~skip_early_reduction_no_dtree ~extra (package_name : Names.Id.t) (rules_proofs : EConstr.t) =
+  let env = Global.env () in
+  let (sigma, include_interp) = Evd.fresh_global env sigma (if include_interp then r_true () else r_false ()) in
+  let (sigma, skip_early_reduction) = Evd.fresh_global env sigma (if skip_early_reduction then r_true () else r_false ()) in
+  let (sigma, skip_early_reduction_no_dtree) = Evd.fresh_global env sigma (if skip_early_reduction_no_dtree then r_true () else r_false ()) in
+  let (sigma, rules_proofs) = rewriter_heuristic_process_rules_proofs env sigma ~poly rules_proofs in
+  let (sigma, scraped_data) = rewriter_scrape_data env sigma ~poly rules_proofs extra in
+  let (sigma, (base, ident, raw_ident, pattern_ident)) = rewriter_emit_inductives sigma ~poly scraped_data None None None None in
+  let (sigma, rewriter) = make_rewriter_of_scraped_and_ind sigma ~poly package_name scraped_data var_like_idents base ident raw_ident pattern_ident include_interp skip_early_reduction skip_early_reduction_no_dtree rules_proofs in
+  (sigma, rewriter)
+
+let vernac_rewriter_emit_inductives ~poly (scraped_data : Constrexpr.constr_expr) (base : Names.Id.t) (ident : Names.Id.t) (raw_ident : Names.Id.t) (pattern_ident : Names.Id.t) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, scraped_data) = Constrintern.interp_constr_evars env sigma scraped_data in
+  ignore(rewriter_emit_inductives sigma ~poly scraped_data (Some base) (Some ident) (Some raw_ident) (Some pattern_ident))
+
+
+let vernac_make_rewriter ~poly ?(var_like_idents = None) ?(include_interp = false) ?(skip_early_reduction = false) ?(skip_early_reduction_no_dtree = true) ?(extra = None) (package_name : Names.Id.t) (rules_proofs : Constrexpr.constr_expr) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, var_like_idents) = match var_like_idents with
+    | Some v -> Constrintern.interp_constr_evars env sigma v
+    | None -> Evd.fresh_global env sigma (r_ident_list_nil ())
+  in
+  let (sigma, extra) = match extra with
+    | Some v -> Constrintern.interp_constr_evars env sigma v
+    | None -> Evd.fresh_global env sigma (r_false ()) (* can be any well-typed term; all subterms get added to the identifiers of the reified language *)
+  in
+  let (sigma, rules_proofs) = Constrintern.interp_constr_evars env sigma rules_proofs in
+  ignore(make_rewriter sigma package_name rules_proofs ~poly ~var_like_idents ~include_interp ~skip_early_reduction ~skip_early_reduction_no_dtree ~extra)
diff --git a/src/Rewriter/Util/plugins/rewriter_build.mli.v818 b/src/Rewriter/Util/plugins/rewriter_build.mli.v818
new file mode 100644
index 000000000..50812a9f9
--- /dev/null
+++ b/src/Rewriter/Util/plugins/rewriter_build.mli.v818
@@ -0,0 +1,3 @@
+val vernac_rewriter_emit_inductives : poly:bool -> Constrexpr.constr_expr -> Names.Id.t -> Names.Id.t -> Names.Id.t -> Names.Id.t -> unit
+
+val vernac_make_rewriter : poly:bool -> ?var_like_idents:(Constrexpr.constr_expr option) -> ?include_interp:bool -> ?skip_early_reduction:bool -> ?skip_early_reduction_no_dtree:bool -> ?extra:(Constrexpr.constr_expr option) -> Names.Id.t -> Constrexpr.constr_expr -> unit
diff --git a/src/Rewriter/Util/plugins/rewriter_build_plugin.mlg.v818 b/src/Rewriter/Util/plugins/rewriter_build_plugin.mlg.v818
new file mode 100644
index 000000000..97736a141
--- /dev/null
+++ b/src/Rewriter/Util/plugins/rewriter_build_plugin.mlg.v818
@@ -0,0 +1,82 @@
+{
+
+open Stdarg
+open Rewriter_build
+
+}
+
+DECLARE PLUGIN "coq-rewriter.rewriter_build"
+
+VERNAC COMMAND EXTEND RewriterEmitInductives CLASSIFIED AS SIDEFF
+  | [ "Rewriter" "Emit" "Inductives" "From" "Scraped" constr(scraped_data) "As" ident(base_ind) ident(ident_ind) ident(raw_ident_ind) ident(pattern_ident_ind) ] -> {
+    let poly = false in
+    vernac_rewriter_emit_inductives ~poly scraped_data base_ind ident_ind raw_ident_ind pattern_ident_ind
+  }
+END
+
+VERNAC COMMAND EXTEND MakeRewriter CLASSIFIED AS SIDEFF
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~include_interp:true
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+  | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
+    let poly = false in
+    vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
+  }
+END
diff --git a/src/Rewriter/Util/plugins/rewriter_build_plugin.mllib.v818 b/src/Rewriter/Util/plugins/rewriter_build_plugin.mllib.v818
new file mode 100644
index 000000000..040c1d139
--- /dev/null
+++ b/src/Rewriter/Util/plugins/rewriter_build_plugin.mllib.v818
@@ -0,0 +1,4 @@
+Definition_by_tactic
+Inductive_from_elim
+Rewriter_build
+Rewriter_build_plugin
diff --git a/src/Rewriter/Util/plugins/strategy_tactic.ml.v818 b/src/Rewriter/Util/plugins/strategy_tactic.ml.v818
new file mode 100644
index 000000000..1cd321189
--- /dev/null
+++ b/src/Rewriter/Util/plugins/strategy_tactic.ml.v818
@@ -0,0 +1,7 @@
+let tclSTRATEGY ~local v (q : Names.GlobRef.t list) =
+  Proofview.Goal.enter begin
+    fun gl ->
+      let env = Proofview.Goal.env gl in
+      Redexpr.set_strategy local [(Conv_oracle.Level v, List.map (Tacred.evaluable_of_global_reference env) q)];
+      Proofview.tclUNIT ()
+  end
diff --git a/src/Rewriter/Util/plugins/strategy_tactic.mli.v818 b/src/Rewriter/Util/plugins/strategy_tactic.mli.v818
new file mode 100644
index 000000000..046af4241
--- /dev/null
+++ b/src/Rewriter/Util/plugins/strategy_tactic.mli.v818
@@ -0,0 +1 @@
+val tclSTRATEGY : local:bool -> int -> Names.GlobRef.t list -> unit Proofview.tactic
diff --git a/src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg.v818 b/src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg.v818
new file mode 100644
index 000000000..32d2d4282
--- /dev/null
+++ b/src/Rewriter/Util/plugins/strategy_tactic_plugin.mlg.v818
@@ -0,0 +1,18 @@
+{
+
+open Ltac_plugin
+open Stdarg
+open Strategy_tactic
+
+}
+
+DECLARE PLUGIN "coq-rewriter.strategy_tactic"
+
+
+(* might be better to do strategy_level(v) ne_smart_global_list(q), but I can't get that working *)
+TACTIC EXTEND strategy
+ | [ "strategy" int(v) "[" ne_reference_list(q) "]"  ] -> {
+   let local = true in
+   tclSTRATEGY ~local v q
+ }
+END
diff --git a/src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib.v818 b/src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib.v818
new file mode 100644
index 000000000..aae0bd65a
--- /dev/null
+++ b/src/Rewriter/Util/plugins/strategy_tactic_plugin.mllib.v818
@@ -0,0 +1,2 @@
+Strategy_tactic
+Strategy_tactic_plugin