"rewrite_strat strat with db" syntax

doc/sphinx/addendum/generalized-rewriting.rst

@@ -795,6 +795,11 @@ Usage
    :tacn:`setoid_rewrite` :n:`@one_term` is basically equivalent to
    :n:`rewrite_strat outermost @one_term`.
 
+.. tacn:: rewrite_strat @rewstrategy with @ident
+
+   Equivalent to :tacn:`rewrite_strat` but the hint database
+   :n:`@ident` is used in typeclass inference instead of
+   `typeclasses_db`.
 
 .. tacn:: rewrite_db @ident__1 {? in @ident__2 }
 

doc/tools/docgram/fullGrammar

@@ -1711,6 +1711,7 @@ simple_tactic: [
 | "compare" constr constr
 | "rewrite_strat" rewstrategy "in" hyp
 | "rewrite_strat" rewstrategy
+| "rewrite_strat" rewstrategy "with" preident
 | "rewrite_db" preident "in" hyp
 | "rewrite_db" preident
 | "substitute" orient glob_constr_with_bindings

doc/tools/docgram/orderedGrammar

@@ -1464,6 +1464,7 @@ simple_tactic: [
 | "is_ground" one_term
 | "autoapply" one_term "with" ident
 | "rewrite_strat" rewstrategy OPT ( "in" ident )
+| "rewrite_strat" rewstrategy "with" ident
 | "rewrite_db" ident OPT ( "in" ident )
 | "substitute" OPT [ "->" | "<-" ] one_term_with_bindings
 | "setoid_rewrite" OPT [ "->" | "<-" ] one_term_with_bindings OPT ( "at" rewrite_occs ) OPT ( "in" ident )

plugins/ltac/g_rewrite.mlg

@@ -141,6 +141,7 @@ let cl_rewrite_clause (ist, c) b occ cl =
 TACTIC EXTEND rewrite_strat
 | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
 | [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
+| [ "rewrite_strat" rewstrategy(s) "with" preident(db) ] -> { cl_rewrite_clause_strat ~db s None }
 | [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) }
 | [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None }
 END

tactics/rewrite.ml

@@ -1482,7 +1482,7 @@ let () = CErrors.register_handler begin function
 | _ -> None
 end
 
-let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
+let cl_rewrite_clause_aux ?(abs=None) ~db strat env avoid sigma concl is_hyp : result =
   let sigma, sort = Typing.sort_of env sigma concl in
   let evdref = ref sigma in
   let evars = (!evdref, Evar.Set.empty) in
@@ -1503,7 +1503,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
   | Identity -> Some None
   | Success res ->
     let (_, cstrs) = res.rew_evars in
-    let evars = solve_constraints ~db:TC.typeclasses_db env res.rew_evars in
+    let evars = solve_constraints ~db env res.rew_evars in
     let iter ev = if not (Evd.is_defined evars ev) then raise (UnsolvedConstraints (env, evars, ev)) in
     let () = Evar.Set.iter iter cstrs in
     let newt = res.rew_to in
@@ -1533,7 +1533,7 @@ let newfail n s =
   let info = Exninfo.reify () in
   Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
 
-let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
+let cl_rewrite_clause_newtac ?abs ?origsigma ~db ~progress strat clause =
   let open Proofview.Notations in
   (* For compatibility *)
   let beta = Tactics.reduct_in_concl ~cast:false ~check:false
@@ -1598,7 +1598,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
     in
     try
       let res =
-        cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
+        cl_rewrite_clause_aux ?abs ~db strat env Id.Set.empty sigma ty clause
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
       treat sigma res state <*>
@@ -1615,11 +1615,12 @@ let tactic_init_setoid () =
     let _, info = Exninfo.capture e in
     Tacticals.tclFAIL ~info (str"Setoid library not loaded")
 
-let cl_rewrite_clause_strat progress strat clause =
+let cl_rewrite_clause_strat ~db progress strat clause =
+  let db = Option.default TC.typeclasses_db db in
   tactic_init_setoid () <*>
   (if progress then Proofview.tclPROGRESS else fun x -> x)
    (Proofview.tclOR
-      (cl_rewrite_clause_newtac ~progress strat clause)
+      (cl_rewrite_clause_newtac ~db ~progress strat clause)
       (fun (e, info) -> match e with
        | Tacticals.FailError (n, pp) ->
          tclFAILn ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
@@ -1629,11 +1630,11 @@ let cl_rewrite_clause_strat progress strat clause =
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
-    cl_rewrite_clause_strat true strat clause
+    cl_rewrite_clause_strat ~db:None true strat clause
 
 (** Setoid rewriting when called with "rewrite_strat" *)
-let cl_rewrite_clause_strat strat clause =
-  cl_rewrite_clause_strat false strat clause
+let cl_rewrite_clause_strat ?db strat clause =
+  cl_rewrite_clause_strat ~db false strat clause
 
 let apply_glob_constr ((_, c) : _ * EConstr.t delayed_open) l2r occs = (); fun ({ state = () ; env = env } as input) ->
   let c sigma =
@@ -1871,7 +1872,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
       (tclPROGRESS
         (tclTHEN
            (Proofview.Unsafe.tclEVARS evd)
-            (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
+            (cl_rewrite_clause_newtac ~db:TC.typeclasses_db ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
     (fun (e, info) -> match e with
     | e -> Proofview.tclZERO ~info e)
   end

tactics/rewrite.mli

@@ -69,7 +69,7 @@ val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('a, 'b) strategy_ast -> Pp.t
 
 (** Entry point for user-level "rewrite_strat" *)
-val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
+val cl_rewrite_clause_strat : ?db:string -> strategy -> Id.t option -> unit Proofview.tactic
 
 (** Entry point for user-level "setoid_rewrite" *)
 val cl_rewrite_clause :