diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 15:46:19 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 15:46:19 +0200 |
commit | 78c0fa183b906aec84bd2e393de0233008b308c4 (patch) | |
tree | 23cf070d0d199d0a474c6b36262dcc22d0b30548 /plugins/ssr/ssrcommon.ml | |
parent | d4d33ecae807deb850c4da187359f46892e90b64 (diff) | |
parent | f6b297b4c068adadf86e77da533782852cfae373 (diff) |
Merge PR #7237: [ssr] fix delayed clears (fix #7045)
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 7 |
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 = |