Merge PR #9153: [api] Move reduction modules to `tactics`

7 files changed, 13 insertions, 25 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 07f50f6cd5..4d817625f5 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -164,11 +164,12 @@ module Btauto = struct
 
   let reify env t = lapp eval [|convert_env env; convert t|]
 
-  let print_counterexample p env gl =
+  let print_counterexample p penv gl =
     let var = lapp witness [|p|] in
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
-    let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
+    let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in
+    let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in
     let var = EConstr.Unsafe.to_constr var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | App (c, _)
@@ -192,7 +193,7 @@ module Btauto = struct
     let msg =
       try
         let var = to_list var in
-        let assign = List.combine env var in
+        let assign = List.combine penv var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
           let sigma, env = Pfedit.get_current_context () in
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 37fc81ee38..ea86a4b514 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -132,7 +132,7 @@ let normalize_evaluables=
 open Ppconstr
 open Printer
 let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
-let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
+let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x)))
 let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
 
 let warn_deprecated_syntax =
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 156ee94a66..5d5d45c58f 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -314,7 +314,7 @@ END
 
 let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
 
-let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
+let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl
 let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
 let in_clause' = Pltac.in_clause
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 2267d43d93..5e3f4df192 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -22,8 +22,8 @@ open Tactypes
 open Locus
 open Decl_kinds
 open Genredexpr
-open Pputils
 open Ppconstr
+open Pputils
 open Printer
 
 open Genintern
@@ -159,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) =
           end
         | _ -> default
 
-  let pr_with_occurrences pr c = pr_with_occurrences pr keyword c
-  let pr_red_expr pr c = pr_red_expr pr keyword c
+  let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c
+  let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c
 
   let pr_may_eval test prc prlc pr2 pr3 = function
     | ConstrEval (r,c) ->
@@ -186,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_and_short_name pr (c,_) = pr c
 
-  let pr_or_by_notation f = CAst.with_val (function
-    | AN v -> f v
-    | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
-
-  let pr_located pr (_,x) = pr x
-
   let pr_evaluable_reference = function
     | EvalVarRef id -> pr_id id
     | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
@@ -694,7 +688,7 @@ let pr_goal_selector ~toplevel s =
         (*  match t with
             | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
             | _ ->*)
-        let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+        let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
         spc() ++ hov 1 (str"(" ++ s ++ str")") in
 
       let pr_fix_tac (id,n,c) =
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0ab9e501bc..bc47036d92 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -98,8 +98,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 83f563e2ab..30e316b36d 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -270,7 +270,7 @@ constraint 'a = <
 
 type g_trm = Genintern.glob_constr_and_expr
 type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
+type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
@@ -296,9 +296,6 @@ type glob_tactic_arg =
 
 (** Raw tactics *)
 
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = qualid or_by_notation
 type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index da0ecfc449..8b6b14322b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -269,7 +269,7 @@ constraint 'a = <
 
 type g_trm = Genintern.glob_constr_and_expr
 type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
+type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
@@ -295,9 +295,6 @@ type glob_tactic_arg =
 
 (** Raw tactics *)
 
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = qualid or_by_notation
 type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel