aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrvernac.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 876751911b..940defb743 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -360,7 +360,7 @@ let coerce_search_pattern_to_sort hpat =
Pattern.PApp (fp, args') in
let hr, na = splay_search_pattern 0 hpat in
let dc, ht =
- let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+ let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in
Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
let np = List.length dc in
if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else