fixing the failure behavior.

src/g_ltac_iter.ml4

@@ -128,17 +128,20 @@ struct
               ++ pr_collection c)
     in resolve_collection
 
-  let the_tactic combiner dbs tacK =
+  let the_tactic (combiner, unit) dbs tacK =
     List.fold_right (fun db acc ->
         resolve_collection combiner tacK acc false db)
-       dbs (Proofview.tclUNIT ())
-
-  let first_combiner a b =
-    Proofview.tclORELSE a (fun _ -> b)
-  let seq_combiner a b =
-    Proofview.tclBIND a (fun _ -> b)
-  let plus_combiner a b =
-    Proofview.tclOR a (fun _ -> b)
+       dbs unit
+
+  let first_combiner =
+    ((fun a b -> Proofview.tclORELSE a (fun _ -> b)),
+     Tacticals.New.tclFAIL 0 Pp.(str "no applicable tactic"))
+  let seq_combiner =
+    ((fun a b -> Proofview.tclBIND a (fun _ -> b)),
+     Proofview.tclUNIT ())
+  let plus_combiner =
+    ((fun a b -> Proofview.tclOR a (fun _ -> b)),
+     Tacticals.New.tclFAIL 0 Pp.(str "no applicable tactic"))
 
 end
 

test-suite/example.v

@@ -28,6 +28,12 @@ Goal False -> True -> 1 = 1 -> True.
   first_of [ *|- ] k.
 Defined.
 
+Goal True -> False -> 1 = 1 -> False.
+  intros.
+  let k l := (apply l) in
+  first_of [ *|- ] k.
+Defined.
+
 Goal False -> True -> 1 = 1 -> True.
   intros.
   let k l := pose l in