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 +-
 tactics/tactics.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 67bf8d0d29..decf19588f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1555,7 +1555,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       | Some proj ->
           let args = Context.Rel.to_extended_vect mkRel 0 sign in
           let proj =
-            match Recordops.find_primitive_projection proj with
+            match Structures.PrimitiveProjections.find_opt proj with
             | Some proj ->
               mkProj (Projection.make proj false, mkApp (c, args))
             | None ->
@@ -1585,7 +1585,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
         let params = List.map EConstr.of_constr params in
         let cstr = (get_constructors env indf).(0) in
         let elim =
-          try DefinedRecord (Recordops.lookup_projections ind)
+          try DefinedRecord (Structures.Structure.find_projections ind)
           with Not_found ->
             let u = EInstance.kind sigma u in
             let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
-- 
cgit v1.2.3