From e8fab6b839e19da231333ca8173bbb2a3d8a4033 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 11 Feb 2017 21:59:58 -0500 Subject: split the algebra library; use fsatz more --- src/Util/Tactics.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index c83790acc..5f7ad65cc 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -28,6 +28,16 @@ Ltac contains search_for in_term := | appcontext[search_for] => idtac end. +Ltac debuglevel := constr:(0%nat). + +Ltac solve_debugfail tac := + solve [tac] || + let dbg := debuglevel in + match dbg with + | O => idtac + | _ => match goal with |- ?G => idtac "couldn't prove" G end + end. + Ltac set_evars := repeat match goal with | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) -- cgit v1.2.3