Prevent hard fails during failed proofs

Author: shilangyu

Solver.v

@@ -177,7 +177,7 @@ Ltac2 find_contradiction hyps_map: constr :=
     | name :: rest =>
       Control.plus (fun _=> try_contra hyps_map name) (fun _ => try_contras hyps_map rest)
     | [] =>
-      Control.throw (Tactic_failure (Some (fprintf "No contradiction found")))
+      Control.zero (Tactic_failure (Some (fprintf "No contradiction found")))
     end in
   try_contras hyps_map (List.map fst (FMap.bindings hyps_map)).
 

Tests.v

@@ -209,6 +209,12 @@ Section Tests.
     strict_order lt.
   Qed.
 
+  (* make sure we can `try` failed solving *)
+  Goal False.
+  Proof.
+    try (strict_order lt).
+  Abort.
+
   (* ---- Long chains ---- *)
 
   (* 10-element chain *)