diff options
author | 2017-07-17 07:47:31 +0200 | |
---|---|---|
committer | 2017-07-17 07:47:31 +0200 | |
commit | 3a5dd0df47b83a1a46061f2a14761d3d9ad79fcb (patch) | |
tree | 843408d6fa6a37307c0441d7fa81b3df6ae277e2 /plugins/ssr/ssrvernac.ml4 | |
parent | 0c297ad43bd4b0b8187aa56756334bd294a212ca (diff) | |
parent | b21cd4620e0983a23dd11c0f582bf367662aeee3 (diff) |
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Diffstat (limited to 'plugins/ssr/ssrvernac.ml4')
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 4c8827bf8..cb6a2cd69 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -337,7 +337,8 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in + let hr, _ = Global.type_of_global_in_context (Global.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 let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in |