More expressive debugging in handle_reified_rewrite_rules_interp (#132

)
mit-plv · Dec 9, 2023 · 90549d8 · 90549d8
1 parent 22162aa
commit 90549d8
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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 _ :=