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]

---
 tactics/hints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5e9c3baeb1..31b276bb3e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -320,7 +320,7 @@ let strip_params env sigma c =
   | App (f, args) ->
     (match EConstr.kind sigma f with
     | Const (cst,_) ->
-      (match Recordops.find_primitive_projection cst with
+      (match Structures.PrimitiveProjections.find_opt cst with
        | Some p ->
          let p = Projection.make p false in
          let npars = Projection.npars p in
-- 
cgit v1.2.3