diff options
| author | Hugo Herbelin | 2016-04-02 21:24:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-03 12:35:30 +0200 |
| commit | 856780b163fdcd5e36a1d4af99034e3af6fde1d7 (patch) | |
| tree | 31340f77867da9914209b2ed240dac88ac82ddb9 | |
| parent | dc36fd7fe118136277d8dc525c528fef38b46d70 (diff) | |
Fixing the "No applicable tactic" non informative error message
regression on apply.
| -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 |