diff options
| author | Maxime Dénès | 2018-10-31 17:15:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 17:16:53 +0100 |
| commit | 6eef3e1faf627b2b67d1428c154acd854ed77b5a (patch) | |
| tree | 9eb37126199fb409712bb1718a1c68b367e6f0c9 /plugins | |
| parent | c25f2b7d14aa522dd6e2ec7da7cbb9dddbc6688b (diff) | |
Clarify meaning of boolean in IPatDispatch
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 931f7044d4..a786b9953d 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -84,7 +84,7 @@ type ssripat = | IPatId of (*TODO id_mod option * *) Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) - | IPatDispatch of bool (* if false and the second argument is [[]] then don't check that the number of goals is 1 *) * ssripatss (* (..|..) *) + | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss (* (..|..) *) | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 71b5b6af3e..0553260472 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -217,7 +217,7 @@ let rec ipat_tac1 ipat : unit tactic = Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id ~conclusion:(fun ~to_clear:clr -> intro_clear clr) - | IPatDispatch(false,[[]]) -> + | IPatDispatch(true,[[]]) -> tclUNIT () | IPatDispatch(_,ipatss) -> tclDISPATCH (List.map ipat_tac ipatss) @@ -278,7 +278,7 @@ let split_at_first_case ipats = loop [] ipats let ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch(false, l)) + | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) | x -> x let option_to_list = function None -> [] | Some x -> [x] |