diff options
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f23808f6f9..28aed8a10e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1429,7 +1429,8 @@ let descend_in_conjunctions avoid tac (err, info) c = with Not_found -> let elim = build_case_analysis_scheme env sigma (ind,u) false sort in NotADefinedRecordUseScheme (snd elim) in - Tacticals.New.tclFIRST + Tacticals.New.tclORELSE0 + (Tacticals.New.tclFIRST (List.init n (fun i -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1442,7 +1443,8 @@ let descend_in_conjunctions avoid tac (err, info) c = [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] - end)) + end))) + (Proofview.tclZERO ~info err) | None -> Proofview.tclZERO ~info err with RefinerError _|UserError _ -> Proofview.tclZERO ~info err end |