From bf5f0520cf105afb048c6eac5d6de1d3e1a719df Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 21:06:34 +0200
Subject: Remove one call to Global.env in Detyping

One other call still remains, but will require to refactor some
section-handling code.
---
 plugins/ssr/ssrview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

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 =
-- 
cgit v1.2.3