From c233a13620202790fa59fc720b7149a0d88f275a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Oct 2020 14:11:39 +0100
Subject: Fixing interpretation of rewrite_strat argument in Ltac.

Ltac variables were not yet supported.
---
 test-suite/success/rewrite_strat.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite/success')

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