From 2af78d3cca0f941841394b224b96f86903a68b10 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 20:40:27 +0200 Subject: [api] Misctypes removal: multi to tactics/rewrite --- plugins/ltac/g_tactic.ml4 | 12 ++++++------ plugins/ltac/pptactic.ml | 2 +- plugins/ltac/tacexpr.ml | 2 +- plugins/ltac/tacexpr.mli | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins/ltac') 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" -- cgit v1.2.3