[api] Misctypes removal: multi to tactics/rewrite

7 files changed, 21 insertions, 15 deletions

diff --git a/library/misctypes.ml b/library/misctypes.ml
index cfae07484..ac8c7890c 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -106,9 +106,3 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-
-type multi =
-  | Precisely of int
-  | UpTo of int
-  | RepeatStar
-  | RepeatPlus
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index dc9f607cf..15db4ca6a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -494,12 +494,12 @@ GEXTEND Gram
     | -> None ] ]
   ;
   rewriter :
-    [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
-      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
-      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
-      | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
-      | c = constr_with_bindings_arg -> (Precisely 1, c)
+    [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c)
+      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c)
+      | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      | c = constr_with_bindings_arg -> (Equality.Precisely 1, c)
       ] ]
   ;
   oriented_rewriter :
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b29af6680..894d91258 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -493,7 +493,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_orient b = if b then mt () else str "<- "
 
-  let pr_multi = function
+  let pr_multi = let open Equality in function
     | Precisely 1 -> mt ()
     | Precisely n -> int n ++ str "!"
     | UpTo n -> int n ++ str "?"
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 17f5e5d41..d6f7a461b 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 17f5e5d41..d6f7a461b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d7e697aed..c91758787 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ccf454c3e..9395cf4a8 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -61,6 +61,12 @@ val general_rewrite_in          :
 val general_rewrite_clause :
   orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 val general_multi_rewrite :
   evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic