diff options
| author | coqbot-app[bot] | 2020-11-20 08:51:20 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 08:51:20 +0000 |
| commit | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (patch) | |
| tree | 3b67df9afab90f5ae1d2aeddd3773a544dcbca95 /plugins | |
| parent | f264aabf59866ae0d18509a7757e69c26e82f508 (diff) | |
| parent | 7265df1cda297603cb4eb74362df4463171c316a (diff) | |
Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index bd514f15d5..a4aa08300d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = - List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in + List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be |