From 115fe6ba6f77cabe8729cc39ec9c373c3b0173d3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 11:10:40 +0100
Subject: 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.
---
 plugins/ssrmatching/ssrmatching.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3