aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrview.ml')
-rw-r--r--plugins/ssr/ssrview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 29a936381..faebe3179 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p =
let mkGHole =
DAst.make
- (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+ (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
let mkGApp f args =
if args = [] then f