diff options
| author | Hugo Herbelin | 2020-11-15 11:10:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-19 20:43:42 +0100 |
| commit | 115fe6ba6f77cabe8729cc39ec9c373c3b0173d3 (patch) | |
| tree | 73081ad04d0f72f88d7bedbcd93552475bc3174e /plugins | |
| parent | a27fb3c67238cc41dc24308a233a02422e0f83f3 (diff) | |
Use a proper canonical structure entry for projections.
This is to make more explicit that arguments of the projection are not
kept.
We seize this opportunity to use QGlobRef equality on GlobRef.
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 |