aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-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 537fd7d7b4..075ebf006a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -43,7 +43,7 @@ module AdaptorDb = struct
term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
let subst_adaptor ( subst, (k, t as a)) =
- let t' = Detyping.subst_glob_constr subst t in
+ let t' = Detyping.subst_glob_constr (Global.env()) subst t in
if t' == t then a else k, t'
let in_db =