split the algebra library; use fsatz more

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)