diff options
| author | Erik Martin-Dorel | 2019-03-01 17:33:21 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | f13c55b0c031b6ef92f28a3297ccfa0f7dde869d (patch) | |
| tree | 2ec73621b43182a6bafbecb372176f3fe777d269 | |
| parent | c02ac6657863ba08b4c5f52dddf770d864ee6d4c (diff) | |
[ssr] under: Add comment to justify the need for check_numgoals
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 757a7968ca..8bca62a4ff 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -400,7 +400,7 @@ let check_numgoals ?(minus = 0) nh = Proofview.numgoals >>= fun ng -> if nh <> ng then let errmsg = - str"Incorrect number of hints" ++ spc() ++ + str"Incorrect number of tactics" ++ spc() ++ str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++ str", was given "++ int (nh - minus)++str")." in @@ -439,6 +439,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = else let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in + (* Usefulness of check_numgoals: tclDISPATCH would be enough, + except for the error message w.r.t. the number of + provided/expected tactics, as the last one is implied *) check_numgoals ~minus:1 nh <*> Proofview.tclDISPATCH ((List.map (function None -> overtac |