diff options
| -rw-r--r-- | library/misctypes.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.ml4 | 12 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.mli | 6 |
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 |