aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrcommon.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 15:46:19 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 15:46:19 +0200
commit78c0fa183b906aec84bd2e393de0233008b308c4 (patch)
tree23cf070d0d199d0a474c6b36262dcc22d0b30548 /plugins/ssr/ssrcommon.ml
parentd4d33ecae807deb850c4da187359f46892e90b64 (diff)
parentf6b297b4c068adadf86e77da533782852cfae373 (diff)
Merge PR #7237: [ssr] fix delayed clears (fix #7045)
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-rw-r--r--plugins/ssr/ssrcommon.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 06c26edbe..d012fd0df 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -802,8 +802,11 @@ let rec is_name_in_ipats name = function
List.exists (function SsrHyp(_,id) -> id = name) clr
|| is_name_in_ipats name tl
| IPatId id :: tl -> id = name || is_name_in_ipats name tl
- | (IPatCase l | IPatDispatch l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
- | _ :: tl -> is_name_in_ipats name tl
+ | IPatAbstractVars ids :: tl ->
+ CList.mem_f Id.equal name ids || is_name_in_ipats name tl
+ | (IPatCase l | IPatDispatch l | IPatInj l) :: tl ->
+ List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
+ | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl
| [] -> false
let view_error s gv =