aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrast.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrast.mli')
-rw-r--r--plugins/ssr/ssrast.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 5571c5420..6ba937a2f 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -88,7 +88,7 @@ type ssripat =
| 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
- | IPatView of ssrview (* /view *)
+ | IPatView of bool * ssrview (* {}/view (true if the clear is present) *)
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Id.t list