From 4419a101a4f5a108be90cf4e420f0b6961e6caac Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Jan 2021 13:55:23 +0100
Subject: Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724
---
 plugins/ltac/extratactics.mlg | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins')

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
 
 (**********************************************************************)
-- 
cgit v1.2.3