diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 10 |
1 files changed, 10 insertions, 0 deletions
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) |