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
---
 test-suite/success/autorewrite.v | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v
index 71d333d439..0ac62fcdc9 100644
--- a/test-suite/success/autorewrite.v
+++ b/test-suite/success/autorewrite.v
@@ -4,25 +4,35 @@ Axiom Ack0 : forall m : nat, Ack 0 m = S m.
 Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1.
 Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 
-Hint Rewrite Ack0 Ack1 Ack2 : base0.
+Module M.
+  #[export] Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
-Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False.
+  Proof.
+    intros.
+    autorewrite with base0 in H using try (apply H; reflexivity).
+  Qed.
+End M.
+
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
-  autorewrite with base0 in H using try (apply H; reflexivity).
-Qed.
+  Fail autorewrite with base0 in *.
+Abort.
+
+Import M.
 
 Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
   autorewrite with base0 in *.
-    apply H;reflexivity.
+ apply H;reflexivity.
 Qed.
 
 (* Check autorewrite does not solve existing evars *)
 (* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
-Hint Rewrite <- plus_n_O : base1.
+Global Hint Rewrite <- plus_n_O : base1.
 Goal forall y, exists x, y+x = y.
 eexists. autorewrite with base1.
 Fail reflexivity.
-- 
cgit v1.2.3