Merge PR #13284: Fixing interpretation of rewrite_strat argument in Ltac

Reviewed-by: ppedrot

5 files changed, 22 insertions, 22 deletions

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index ee94fd565a..a3f03b5bb5 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -67,12 +67,12 @@ END
 {
 
 type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
+type glob_strategy = (glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast
 
 let interp_strategy ist gl s =
   let sigma = project gl in
-    sigma, strategy_of_ast s
-let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s
+    sigma, strategy_of_ast ist s
+let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (Tacintern.intern_red_expr ist) s
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
@@ -80,12 +80,9 @@ let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) =
   let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
   Rewrite.pr_strategy (prc env sigma) prr s
 let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) =
-  let prr = Pptactic.pr_red_expr env sigma
-    (Ppconstr.pr_constr_expr,
-    Ppconstr.pr_lconstr_expr,
-    Pputils.pr_or_by_notation Libnames.pr_qualid,
-    Ppconstr.pr_constr_expr)
-  in
+  let prpat env sigma (_,c,_) = prc env sigma c in
+  let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in
+  let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prpat) in
   Rewrite.pr_strategy (prc env sigma) prr s
 
 }
@@ -130,15 +127,15 @@ END
 {
 
 let db_strat db = StratUnary (Topdown, StratHints (false, db))
-let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
+let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast ist (db_strat db))
 
 }
 
 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_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) }
-| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db 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
 
 {
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 87da304330..edd56ee0f7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1135,8 +1135,8 @@ let pr_goal_selector ~toplevel s =
         pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
         pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
         pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
-        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
+        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = Pputils.pr_glb_generic;
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a1970cbce2..26e2b18a02 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1638,9 +1638,9 @@ let cl_rewrite_clause l left2right occs clause =
 let cl_rewrite_clause_strat strat clause =
   cl_rewrite_clause_strat false strat clause
 
-let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
+let apply_glob_constr ist c l2r occs = (); fun ({ state = () ; env = env } as input) ->
   let c sigma =
-    let (sigma, c) = Pretyping.understand_tcc env sigma c in
+    let (sigma, c) = Tacinterp.interp_open_constr ist env sigma c in
     (sigma, (c, NoBindings))
   in
   let flags = general_rewrite_unif_flags () in
@@ -1717,12 +1717,12 @@ let rec pr_strategy prc prr = function
 | StratEval r -> str "eval" ++ spc () ++ prr r
 | StratFold c -> str "fold" ++ spc () ++ prc c
 
-let rec strategy_of_ast = function
+let rec strategy_of_ast ist = function
   | StratId -> Strategies.id
   | StratFail -> Strategies.fail
   | StratRefl -> Strategies.refl
   | StratUnary (f, s) ->
-    let s' = strategy_of_ast s in
+    let s' = strategy_of_ast ist s in
     let f' = match f with
       | Subterms -> all_subterms
       | Subterm -> one_subterm
@@ -1736,13 +1736,13 @@ let rec strategy_of_ast = function
       | Repeat -> Strategies.repeat
     in f' s'
   | StratBinary (f, s, t) ->
-    let s' = strategy_of_ast s in
-    let t' = strategy_of_ast t in
+    let s' = strategy_of_ast ist s in
+    let t' = strategy_of_ast ist t in
     let f' = match f with
       | Compose -> Strategies.seq
       | Choice -> Strategies.choice
     in f' s' t'
-  | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
+  | StratConstr (c, b) -> { strategy = apply_glob_constr ist c b AllOccurrences }
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
   | StratTerms l -> { strategy =
     (fun ({ state = () ; env } as input) ->
@@ -1751,7 +1751,7 @@ let rec strategy_of_ast = function
                     }
   | StratEval r -> { strategy =
     (fun ({ state = () ; env ; evars } as input) ->
-     let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
+     let (sigma,r_interp) = Tacinterp.interp_red_expr ist env (goalevars evars) r in
      (Strategies.reduce r_interp).strategy { input with
                                              evars = (sigma,cstrevars evars) }) }
   | StratFold c -> Strategies.fold_glob (fst c)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 60a66dd861..8e0ce183c2 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -62,7 +62,7 @@ type rewrite_result =
 
 type strategy
 
-val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
+val strategy_of_ast : interp_sign -> (glob_constr_and_expr, glob_red_expr) strategy_ast -> strategy
 
 val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fe3079198c..a74f4592f7 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -77,6 +77,9 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac
 val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** Interprets redexp arguments *)
+val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> glob_red_expr -> Evd.evar_map * red_expr
+
+(** Interprets redexp arguments from a raw one *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
 
 (** Interprets tactic expressions *)