diff options
Diffstat (limited to 'plugins/ltac/extratactics.mlg')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 90c366ed63..d9da47134d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star { -let add_rewrite_hint ~poly bases ort t lcsr = +let add_rewrite_hint ~locality ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in let f ce = @@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in let eqs = List.map f lcsr in - let add_hints base = add_rew_rules base eqs in + let add_hints base = add_rew_rules ~locality base eqs in List.iter add_hints bases let classify_hint _ = VtSideff ([], VtLater) @@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater) } VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic bl o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:polymorphic bl o (Some t) l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o None l } -| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l } + { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l } +| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l } END (**********************************************************************) |