diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 20:40:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:27 +0200 |
| commit | 2af78d3cca0f941841394b224b96f86903a68b10 (patch) | |
| tree | 915a23629878162399f2d26af37c282f9e73c402 /plugins/ltac | |
| parent | 7e7aa7491e3743abe858c1be6b77bd9a986d4297 (diff) | |
[api] Misctypes removal: multi to tactics/rewrite
Diffstat (limited to 'plugins/ltac')
| -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 |
4 files changed, 9 insertions, 9 deletions
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" |