diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-15 13:18:40 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0a6e65e3cec0a8f00f357d82489532203f315389 (patch) | |
| tree | b7bc706ce46b38e3c43f9375fd5a2dd9859d056a /src/Util/Tactics.v | |
| parent | 0a9ea9df752b078bbd89f765cf760081036bd51a (diff) | |
address some code review comments
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 5f7ad65cc..d98ac1bd4 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -32,11 +32,12 @@ 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. + ( let dbg := debuglevel in + match dbg with + | O => idtac + | _ => match goal with |- ?G => idtac "couldn't prove" G end + end; + fail). Ltac set_evars := repeat match goal with |