diff options
| author | Arnaud Spiwack | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-08 12:52:05 +0200 |
| commit | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (patch) | |
| tree | 3dc155ac0aab0bd845debefc8805cdd1106cd52f /tactics | |
| parent | 0aec33ac7ede9098b5cef9ce467bfad5aca8b379 (diff) | |
Display number of available goals in "incorrect number of goals" error message.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 7c11857baa..600ad86efb 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -342,7 +342,12 @@ module New = struct Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end begin function - | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals") + | SizeMismatch (i,_)-> + let errmsg = + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str" tactics)" + in + tclFAIL 0 errmsg | reraise -> tclZERO reraise end end @@ -360,7 +365,12 @@ module New = struct t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) begin tclDISPATCH l end begin function - | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals") + | SizeMismatch (i,_)-> + let errmsg = + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str" tactics)" + in + tclFAIL 0 errmsg | reraise -> tclZERO reraise end end |