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

6 files changed, 0 insertions, 169 deletions

diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
deleted file mode 100644
index 607f2258fd..0000000000
--- a/interp/genredexpr.ml
+++ /dev/null
@@ -1,65 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Reduction expressions *)
-
-(** The parsing produces initially a list of [red_atom] *)
-
-type 'a red_atom =
-  | FBeta
-  | FMatch
-  | FFix
-  | FCofix
-  | FZeta
-  | FConst of 'a list
-  | FDeltaBut of 'a list
-
-(** This list of atoms is immediately converted to a [glob_red_flag] *)
-
-type 'a glob_red_flag = {
-  rBeta : bool;
-  rMatch : bool;
-  rFix : bool;
-  rCofix : bool;
-  rZeta : bool;
-  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
-  rConst : 'a list
-}
-
-(** Generic kinds of reductions *)
-
-type ('a,'b,'c) red_expr_gen =
-  | Red of bool
-  | Hnf
-  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Cbn of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
-  | Unfold of 'b Locus.with_occurrences list
-  | Fold of 'a list
-  | Pattern of 'a Locus.with_occurrences list
-  | ExtraRedExpr of string
-  | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
-  | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
-
-type ('a,'b,'c) may_eval =
-  | ConstrTerm of 'a
-  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of Names.lident * 'a
-  | ConstrTypeOf of 'a
-
-open Libnames
-open Constrexpr
-
-type r_trm = constr_expr
-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
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/redops.ml b/interp/redops.ml
deleted file mode 100644
index b9a74136e4..0000000000
--- a/interp/redops.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Genredexpr
-
-let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
-
-let make_red_flag l =
-  let rec add_flag red = function
-    | [] -> red
-    | FBeta :: lf -> add_flag { red with rBeta = true } lf
-    | FMatch :: lf -> add_flag { red with rMatch = true } lf
-    | FFix :: lf -> add_flag { red with rFix = true } lf
-    | 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");
-        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");
-        add_flag
-          { red with rConst = union_consts red.rConst l; rDelta = true }
-          lf
-  in
-  add_flag
-    {rBeta = false; rMatch = false; rFix = false; rCofix = false;
-     rZeta = false; rDelta = false; rConst = []}
-    l
-
-
-let all_flags =
-  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
-   rZeta = true; rDelta = true; rConst = []}
-
-(** Mapping [red_expr_gen] *)
-
-let map_flags f flags =
-  { flags with rConst = List.map f flags.rConst }
-
-let map_occs f (occ,e) = (occ,f e)
-
-let map_red_expr_gen f g h = function
-  | Fold l -> Fold (List.map f l)
-  | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
-  | Simpl (flags,occs_o) ->
-     Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
-  | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
-  | Cbv flags -> Cbv (map_flags g flags)
-  | Lazy flags -> Lazy (map_flags g flags)
-  | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
-  | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
-  | Cbn flags -> Cbn (map_flags g flags)
-  | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/interp/redops.mli b/interp/redops.mli
deleted file mode 100644
index 7254f29b25..0000000000
--- a/interp/redops.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Genredexpr
-
-val make_red_flag : 'a red_atom list -> 'a glob_red_flag
-
-val all_flags : 'a glob_red_flag
-
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
-  ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
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