[api] Move reduction modules to `tactics`

These modules do actually belong there.

We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.

28 files changed, 185 insertions, 211 deletions

diff --git a/interp/interp.mllib b/interp/interp.mllib
index aa20bda705..147eaf20dc 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,4 @@
 Constrexpr
-Genredexpr
-Redops
 Tactypes
 Stdarg
 Notation_term
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 7b01b6dc1c..bf3a8fe215 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,8 +11,6 @@
 open Genarg
 open Geninterp
 
-type 'a and_short_name = 'a * Names.lident option
-
 let make0 ?dyn name =
   let wit = Genarg.make0 name in
   let () = register_val0 wit dyn in
@@ -53,8 +51,6 @@ let wit_uconstr = make0 "uconstr"
 
 let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_red_expr = make0 "redexpr"
-
 let wit_clause_dft_concl  =
   make0 "clause_dft_concl"
 
@@ -65,4 +61,3 @@ let wit_preident = wit_pre_ident
 let wit_reference = wit_ref
 let wit_global = wit_ref
 let wit_clause = wit_clause_dft_concl
-let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 5e5e43ed38..c974a4403c 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,15 +14,11 @@ open Loc
 open Names
 open EConstr
 open Libnames
-open Genredexpr
-open Pattern
 open Constrexpr
 open Genarg
 open Genintern
 open Locus
 
-type 'a and_short_name = 'a * lident option
-
 val wit_unit : unit uniform_genarg_type
 
 val wit_bool : bool uniform_genarg_type
@@ -52,11 +48,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
 val wit_open_constr :
   (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_red_expr :
-  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
 val wit_clause_dft_concl :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 
 (** Aliases for compatibility *)
@@ -66,7 +57,3 @@ val wit_preident : string uniform_genarg_type
 val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_redexpr :
-  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
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 55e58187b0..8bf1855fe0 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 2bd21f9d7a..b99f956ce0 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 0c27f3bfe2..bd080bf4f0 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
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6d53349fa1..26202ef4ca 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -14,7 +14,6 @@ open Util
 open Pp
 open CAst
 open Names
-open Nameops
 open Libnames
 open Pputils
 open Ppextend
@@ -230,20 +229,6 @@ let tag_var = tag Tag.variable
     | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-  let pr_lident {loc; v=id} =
-    match loc with
-    | None     -> pr_id id
-    | Some loc -> let (b,_) = Loc.unloc loc in
-                  pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id)
-
-  let pr_lname = function
-    | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
-    | x -> pr_ast Name.print x
-
-  let pr_or_var pr = function
-    | Locus.ArgArg x -> pr x
-    | Locus.ArgVar id -> pr_lident id
-
   let pr_prim_token = function
     | Numeral (n,s) -> str (if s then n else "-"^n)
     | String s -> qs s
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index e7f71849a5..1cb3aa6d7a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
-val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
-
-val pr_lident : lident -> Pp.t
-val pr_lname : lname -> Pp.t
-
 val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
 val pr_com_at : int -> Pp.t
 val pr_sep_com :
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 59e5f68f22..e6daf9544c 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -12,7 +12,6 @@ open Util
 open Pp
 open Genarg
 open Locus
-open Genredexpr
 
 let beautify_comments = ref []
 
@@ -39,91 +38,25 @@ let pr_located pr (loc, x) =
 
 let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v)
 
-let pr_or_var pr = function
-  | ArgArg x -> pr x
-  | ArgVar {CAst.v=s} -> Names.Id.print s
-
-let pr_with_occurrences pr keyword (occs,c) =
-  match occs with
-    | AllOccurrences ->
-      pr c
-    | NoOccurrences ->
-      failwith "pr_with_occurrences: no occurrences"
-    | OnlyOccurrences nl ->
-      hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
-                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
-    | AllOccurrencesBut nl ->
-      hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
-                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
-
-exception ComplexRedFlag
-
-let pr_short_red_flag pr r =
-  if not r.rBeta ||  not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
-    raise ComplexRedFlag
-  else if List.is_empty r.rConst then
-    if r.rDelta then mt () else raise ComplexRedFlag
-  else (if r.rDelta then str "-" else mt ()) ++
-          hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
-
-let pr_red_flag pr r =
-  try pr_short_red_flag pr r
-  with ComplexRedFlag ->
-    (if r.rBeta then pr_arg str "beta" else mt ()) ++
-      (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
-          (if r.rMatch then pr_arg str "match" else mt ()) ++
-          (if r.rFix then pr_arg str "fix" else mt ()) ++
-          (if r.rCofix then pr_arg str "cofix" else mt ())) ++
-      (if r.rZeta then pr_arg str "zeta" else mt ()) ++
-      (if List.is_empty r.rConst then
-          if r.rDelta then pr_arg str "delta"
-          else mt ()
-        else
-          pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
-            hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
-
-let pr_union pr1 pr2 = function
-  | Inl a -> pr1 a
-  | Inr b -> pr2 b
-
-let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
-  | Red false -> keyword "red"
-  | Hnf -> keyword "hnf"
-  | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
-                    ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
-  | Cbv f ->
-    if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
-          f.rZeta && f.rDelta && List.is_empty f.rConst then
-      keyword "compute"
-    else
-      hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
-  | Lazy f ->
-    hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
-  | Cbn f ->
-    hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
-  | Unfold l ->
-    hov 1 (keyword "unfold" ++ spc() ++
-              prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
-  | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
-  | Pattern l ->
-    hov 1 (keyword "pattern" ++
-              pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+let pr_lident { CAst.loc; v=id } =
+  let open Names.Id in
+  match loc with
+  | None     -> print id
+  | Some loc -> let (b,_) = Loc.unloc loc in
+    pr_located print
+      (Some (Loc.make_loc (b,b + String.length (to_string id))), id)
 
-  | Red true ->
-    CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
-  | ExtraRedExpr s ->
-    str s
-  | CbvVm o ->
-    keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
-  | CbvNative o ->
-    keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+let pr_lname = let open Names in function
+  | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
+  | x -> pr_ast Name.print x
 
-let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
-  pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar id -> pr_lident id
 
-let pr_or_by_notation f = let open Constrexpr in function
-  | {CAst.loc; v=AN v} -> f v
-  | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function
+    | AN v -> f v
+    | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
 
 let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 5b1969e232..ea554355bc 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -8,33 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open Genarg
-open Locus
-open Genredexpr
 
 val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
 val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_lident : lident -> Pp.t
+val pr_lname : lname -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
-val pr_with_occurrences :
-  ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
-
-val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
-val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
-
-val pr_red_expr :
-  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
-  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
-
-val pr_red_expr_env : Environ.env -> Evd.evar_map ->
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
-  ('b -> Pp.t) *
-  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
-  (string -> Pp.t) ->
-  ('a,'b,'c) red_expr_gen -> Pp.t
 
 val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
 val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index dbd5be23ab..0ce726db25 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -7,7 +7,6 @@ Logic
 Goal_select
 Proof_bullet
 Proof_global
-Redexpr
 Refiner
 Tacmach
 Pfedit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 64d7630d55..eed68b058b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -15,7 +15,6 @@ open Environ
 open Reductionops
 open Evd
 open Typing
-open Redexpr
 open Tacred
 open Logic
 open Context.Named.Declaration
@@ -71,11 +70,6 @@ let pf_global gls id =
   let sigma = project gls in
   Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id)
 
-let pf_reduction_of_red_expr gls re c =
-  let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
-  let sigma = project gls in
-  redfun (pf_env gls) sigma c
-
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ef6a1544e4..213ed7bfda 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,7 +12,6 @@ open Names
 open Constr
 open Environ
 open EConstr
-open Redexpr
 open Locus
 
 (** Operations for handling terms under a local typing context. *)
@@ -44,9 +43,6 @@ val pf_get_hyp_typ        : Goal.goal sigma -> Id.t -> types
 
 val pf_get_new_id         : Id.t -> Goal.goal sigma -> Id.t
 
-val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr
-
-
 val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a
 val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> 
   Goal.goal sigma -> 'a -> Goal.goal sigma * 'b
diff --git a/interp/genredexpr.ml b/tactics/genredexpr.ml
index 607f2258fd..8209684c37 100644
--- a/interp/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -63,3 +63,17 @@ type r_pat = constr_pattern_expr
 type r_cst = qualid or_by_notation
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+
+let make0 ?dyn name =
+  let wit = Genarg.make0 name in
+  let () = Geninterp.register_val0 wit dyn in
+  wit
+
+type 'a and_short_name = 'a * Names.lident option
+
+let wit_red_expr :
+  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
+   (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
+   (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
+    Genarg.genarg_type =
+  make0 "redexpr"
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
new file mode 100644
index 0000000000..dd1bcd4699
--- /dev/null
+++ b/tactics/ppred.ml
@@ -0,0 +1,83 @@
+open Util
+open Pp
+open Locus
+open Genredexpr
+open Pputils
+
+let pr_with_occurrences pr keyword (occs,c) =
+  match occs with
+    | AllOccurrences ->
+      pr c
+    | NoOccurrences ->
+      failwith "pr_with_occurrences: no occurrences"
+    | OnlyOccurrences nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+    | AllOccurrencesBut nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+exception ComplexRedFlag
+
+let pr_short_red_flag pr r =
+  if not r.rBeta ||  not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+    raise ComplexRedFlag
+  else if List.is_empty r.rConst then
+    if r.rDelta then mt () else raise ComplexRedFlag
+  else (if r.rDelta then str "-" else mt ()) ++
+          hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+let pr_red_flag pr r =
+  try pr_short_red_flag pr r
+  with ComplexRedFlag ->
+    (if r.rBeta then pr_arg str "beta" else mt ()) ++
+      (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+          (if r.rMatch then pr_arg str "match" else mt ()) ++
+          (if r.rFix then pr_arg str "fix" else mt ()) ++
+          (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+      (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+      (if List.is_empty r.rConst then
+          if r.rDelta then pr_arg str "delta"
+          else mt ()
+        else
+          pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+            hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+let pr_union pr1 pr2 = function
+  | Inl a -> pr1 a
+  | Inr b -> pr2 b
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
+  | Red false -> keyword "red"
+  | Hnf -> keyword "hnf"
+  | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+                    ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | Cbv f ->
+    if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+          f.rZeta && f.rDelta && List.is_empty f.rConst then
+      keyword "compute"
+    else
+      hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
+  | Lazy f ->
+    hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+  | Cbn f ->
+    hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+  | Unfold l ->
+    hov 1 (keyword "unfold" ++ spc() ++
+              prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
+  | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+  | Pattern l ->
+    hov 1 (keyword "pattern" ++
+              pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+
+  | Red true ->
+    CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
+  | ExtraRedExpr s ->
+    str s
+  | CbvVm o ->
+    keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | CbvNative o ->
+    keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+
+let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
+  pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
new file mode 100644
index 0000000000..b3a306a36f
--- /dev/null
+++ b/tactics/ppred.mli
@@ -0,0 +1,19 @@
+open Genredexpr
+
+val pr_with_occurrences :
+  ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
+
+val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+
+val pr_red_expr :
+  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
+
+val pr_red_expr_env : Environ.env -> Evd.evar_map ->
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  ('b -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
+  (string -> Pp.t) ->
+  ('a,'b,'c) red_expr_gen -> Pp.t
diff --git a/proofs/redexpr.ml b/tactics/redexpr.ml
index 6658c37f41..aabfae444e 100644
--- a/proofs/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -74,13 +74,13 @@ let set_strategy_one ref l  =
         Csymtable.set_opaque_const sp
     | ConstKey sp, _ ->
         let cb = Global.lookup_constant sp in
-	(match cb.const_body with
-	  | OpaqueDef _ ->
+        (match cb.const_body with
+          | OpaqueDef _ ->
             user_err ~hdr:"set_transparent_const"
               (str "Cannot make" ++ spc () ++
                  Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
-		 spc () ++ str "transparent because it was declared opaque.");
-	  | _ -> Csymtable.set_transparent_const sp)
+                 spc () ++ str "transparent because it was declared opaque.");
+          | _ -> Csymtable.set_transparent_const sp)
     | _ -> ()
 
 let cache_strategy (_,str) =
@@ -126,10 +126,10 @@ type strategy_obj =
 let inStrategy : strategy_obj -> obj =
   declare_object {(default_object "STRATEGY") with
                     cache_function = (fun (_,obj) -> cache_strategy obj);
-		    load_function = (fun _ (_,obj) -> cache_strategy obj);
-		    subst_function = subst_strategy;
+                    load_function = (fun _ (_,obj) -> cache_strategy obj);
+                    subst_function = subst_strategy;
                     discharge_function = discharge_strategy;
-		    classify_function = classify_strategy }
+                    classify_function = classify_strategy }
 
 
 let set_strategy local str =
@@ -154,16 +154,16 @@ let make_flag env f =
   let red =
     if f.rDelta then (* All but rConst *)
         let red = red_add red fDELTA in
-        let red = red_add_transparent red 
+        let red = red_add_transparent red
                     (Conv_oracle.get_transp_state (Environ.oracle env)) in
-	List.fold_right
-	  (fun v red -> red_sub red (make_flag_constant v))
-	  f.rConst red
+        List.fold_right
+          (fun v red -> red_sub red (make_flag_constant v))
+          f.rConst red
     else (* Only rConst *)
         let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in
-	List.fold_right
-	  (fun v red -> red_add red (make_flag_constant v))
-	  f.rConst red
+        List.fold_right
+          (fun v red -> red_add red (make_flag_constant v))
+          f.rConst red
   in red
 
 (* table of custom reductino fonctions, not synchronized,
@@ -234,7 +234,7 @@ let reduction_of_red_expr env =
      let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
      let () =
        if not (!simplIsCbn || List.is_empty f.rConst) then
-	 warn_simpl_unfolding_modifiers () in
+         warn_simpl_unfolding_modifiers () in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
   | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
@@ -246,9 +246,9 @@ let reduction_of_red_expr env =
   | ExtraRedExpr s ->
       (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
-	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
-	 with Not_found ->
-	   user_err ~hdr:"Redexpr.reduction_of_red_expr"
+        (try reduction_of_red_expr (String.Map.find s !red_expr_tab)
+         with Not_found ->
+           user_err ~hdr:"Redexpr.reduction_of_red_expr"
              (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
@@ -270,9 +270,9 @@ let inReduction : bool * string * red_expr -> obj =
        cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
        load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e);
        subst_function =
-	(fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
+        (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
        classify_function =
-	(fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
+        (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
 
 let declare_red_expr locality s expr =
     Lib.add_anonymous_leaf (inReduction (locality,s,expr))
diff --git a/proofs/redexpr.mli b/tactics/redexpr.mli
index 1e59f436c3..1f65862701 100644
--- a/proofs/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -20,7 +20,7 @@ open Locus
 
 type red_expr =
     (constr, evaluable_global_reference, constr_pattern) red_expr_gen
- 
+
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr :
diff --git a/interp/redops.ml b/tactics/redops.ml
index b9a74136e4..6f83ea9a34 100644
--- a/interp/redops.ml
+++ b/tactics/redops.ml
@@ -21,14 +21,14 @@ let make_red_flag l =
     | FCofix :: lf -> add_flag { red with rCofix = true } lf
     | FZeta :: lf -> add_flag { red with rZeta = true } lf
     | FConst l :: lf ->
-	if red.rDelta then
-	  CErrors.user_err Pp.(str
-	    "Cannot set both constants to unfold and constants not to unfold");
+        if red.rDelta then
+          CErrors.user_err Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
         add_flag { red with rConst = union_consts red.rConst l } lf
     | FDeltaBut l :: lf ->
-	if red.rConst <> [] && not red.rDelta then
-	  CErrors.user_err Pp.(str
-	    "Cannot set both constants to unfold and constants not to unfold");
+        if red.rConst <> [] && not red.rDelta then
+          CErrors.user_err Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
         add_flag
           { red with rConst = union_consts red.rConst l; rDelta = true }
           lf
diff --git a/interp/redops.mli b/tactics/redops.mli
index 7254f29b25..7254f29b25 100644
--- a/interp/redops.mli
+++ b/tactics/redops.mli
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b3ea13cf4f..9bd4a29a69 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -889,7 +889,7 @@ let reduce redexp cl =
   let trace env sigma =
     let open Printer in
     let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
-    Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
+    Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
   in
   let trace () =
     let sigma, env = Pfedit.get_current_context () in
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 5afec74fae..1861c5b99b 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -6,6 +6,10 @@ Hipattern
 Ind_tables
 Eqschemes
 Elimschemes
+Genredexpr
+Redops
+Redexpr
+Ppred
 Tactics
 Abstract
 Elim
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e7c1e29beb..46854b7f5d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -700,7 +700,7 @@ open Pputils
           | None -> mt()
           | Some r ->
             keyword "Eval" ++ spc() ++
-              pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
+              Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++
               keyword " in" ++ spc()
         in
         let pr_def_body = function
@@ -1134,7 +1134,7 @@ open Pputils
         let pr_mayeval r c = match r with
           | Some r0 ->
             hov 2 (keyword "Eval" ++ spc() ++
-                     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
+                     Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++
                      spc() ++ keyword "in" ++ spc () ++ pr_lconstr c)
           | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
         in
@@ -1146,7 +1146,7 @@ open Pputils
       | VernacDeclareReduction (s,r) ->
         return (
           keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++
-            pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
+            Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r
         )
       | VernacPrint p ->
         return (pr_printable p)
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index f26e0d0885..a647b2ef73 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e
 let get_command_entry () = !Vernac_.command_entry_ref
 
 let () =
-  register_grammar Stdarg.wit_red_expr (Vernac_.red_expr);
+  register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);