fix guard messages to consider new trace (with tagged rewrites)

marcusrossel · May 25, 2024 · 562c14b · 562c14b
1 parent a62fb1a
commit 562c14b
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 0 deletions.
diff --git a/Lean/Egg/Tests/Conditional.lean b/Lean/Egg/Tests/Conditional.lean
@@ -95,6 +95,7 @@ info: [egg.rewrites] Rewrites
           expr:  [?l₂]
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)

diff --git a/Lean/Egg/Tests/Prune.lean b/Lean/Egg/Tests/Prune.lean
@@ -21,6 +21,7 @@ info: [egg.rewrites] Rewrites
           expr:  []
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)
@@ -55,6 +56,7 @@ info: [egg.rewrites] Rewrites
           expr:  [?n, ?m]
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Hypotheses (0)

diff --git a/Lean/Egg/Tests/TC Proj Binders.lean b/Lean/Egg/Tests/TC Proj Binders.lean
@@ -25,6 +25,7 @@ info: [egg.rewrites] Rewrites
           expr:  []
           class: []
           level: []
+  [egg.rewrites] Tagged (0)
   [egg.rewrites] Generated (2)
     [egg.rewrites] #0[0?69632,0](⇔)
       [egg.rewrites] HMul.hMul = Mul.mul