From 34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 18 Mar 2021 19:15:39 +0100
Subject: [recordops] complete API rewrite; the module is now called
 [structures]

---
 vernac/comSearch.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comSearch.ml')

diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
index 1b811f3db7..39520a68ec 100644
--- a/vernac/comSearch.ml
+++ b/vernac/comSearch.ml
@@ -41,8 +41,8 @@ let kind_searcher = Decls.(function
     Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr &&
                                       (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions)
   | IsDefinition CanonicalStructure ->
-    let canonproj = Recordops.canonical_projections () in
-    Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj)
+    let canonproj = Structures.CSTable.entries () in
+    Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Structures.CSTable.solution gr) canonproj)
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
     Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes)
-- 
cgit v1.2.3