diff --git a/src/g_ltac_iter.ml4 b/src/g_ltac_iter.ml4 index 8d2fd2f..6cafa0a 100644 --- a/src/g_ltac_iter.ml4 +++ b/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 diff --git a/test-suite/example.v b/test-suite/example.v index 048cee0..6794119 100644 --- a/test-suite/example.v +++ b/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