diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
index 10ed407f3..fadb8c707 100644
--- a/src/Rewriter/Rewriter/ProofsCommonTactics.v
+++ b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -568,7 +568,8 @@ Module Compilers.
       | idtac "============================";
         idtac "WARNING: UNSOLVED INITIAL GOAL:";
         print_context_and_goal ();
-        idtac "============================" ].
+        idtac "============================";
+        idtac "Failed to solve goal with" "repeat" "Rewriter.ProofsCommonTactics.Compilers.RewriteRules.InterpTactics.handle_reified_rewrite_rules_interp_step" exprInfo exprExtraInfo base_interp_head ident_interp_head ident_interp_Proper ].
 
       Module Export Tactic.
         Ltac prove_interp_good _ :=