diff options
| author | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
| commit | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (patch) | |
| tree | 865bd07aa81debed13d6c5b5f4b5b2d8d26d7443 /plugins/ssr | |
| parent | 69cbb9c09d5a440461b945c6690745b444649fda (diff) | |
| parent | 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 (diff) | |
Merge PR #8687: Mini reorganization type of global constr of global
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 |
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 |