diff options
| author | Maxime Dénès | 2019-04-04 21:06:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | bf5f0520cf105afb048c6eac5d6de1d3e1a719df (patch) | |
| tree | dfc7afd2f394958a81c5ce33d1422f72b7e6b36b /plugins/ssr | |
| parent | 3b980d937b5adfbae472ed8a13748a451fdf3450 (diff) | |
Remove one call to Global.env in Detyping
One other call still remains, but will require to refactor some
section-handling code.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 2 |
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 = |