test-suite/bugs/closed/bug_10972.v


1
2
3
4
5
6
7
8
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.