Fixing interpretation of rewrite_strat argument in Ltac.

Ltac variables were not yet supported.

2 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10972.v b/test-suite/bugs/closed/bug_10972.v
new file mode 100644
index 0000000000..945c23c9a4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10972.v
@@ -0,0 +1,9 @@
+(* Check rewrite_strat is compatible with Ltac *)
+Require Import Coq.Setoids.Setoid.
+Module foo.
+  Definition Foo := True.
+  Ltac foo := rewrite_strat eval cbv [Foo].
+End foo.
+Goal foo.Foo.
+  foo.foo.
+Abort.
diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v
index a6e59fdda0..98045d1162 100644
--- a/test-suite/success/rewrite_strat.v
+++ b/test-suite/success/rewrite_strat.v
@@ -51,3 +51,12 @@ Time Qed. (* 0.06 s *)
 
 Set Printing All.
 Set Printing Depth 100000.
+
+Tactic Notation "my_rewrite_strat" constr(x) := rewrite_strat topdown x.
+Tactic Notation "my_rewrite_strat2" uconstr(x) := rewrite_strat topdown x.
+Goal (forall x, S x = 0) -> 1=0.
+intro H.
+my_rewrite_strat H.
+Undo.
+my_rewrite_strat2 H.
+Abort.