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.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d..6ba937a2f 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
@@ -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