From 90549d8f0910d4d5c7a28bfd0266e5dc719a51dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Dec 2023 19:47:21 -0800 Subject: [PATCH] More expressive debugging in `handle_reified_rewrite_rules_interp` (#132) --- src/Rewriter/Rewriter/ProofsCommonTactics.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 _ :=