diff options
| author | Pierre-Marie Pédrot | 2021-01-19 10:02:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-19 10:02:32 +0100 |
| commit | 326df6dc176f70b3192f463164c3a435ab187bed (patch) | |
| tree | 8721d463b0f41e5134e823c756b72a936c4df607 /plugins | |
| parent | f44e65e0d209fdada20998d661ad10a5e82a0d92 (diff) | |
| parent | 4419a101a4f5a108be90cf4e420f0b6961e6caac (diff) | |
Merge PR #13725: Support locality attributes for Hint Rewrite (including export)
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -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 (**********************************************************************) |