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]

---
 library/globnames.ml  | 4 ----
 library/globnames.mli | 1 -
 2 files changed, 5 deletions(-)

(limited to 'library')

diff --git a/library/globnames.ml b/library/globnames.ml
index 654349dea0..491c89e68e 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,10 +31,6 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
-let subst_constructor subst (ind,j as ref) =
-  let ind' = subst_ind subst ind in
-  if ind==ind' then ref
-  else (ind',j)
 
 let subst_global_reference subst ref = match ref with
   | VarRef var -> ref
diff --git a/library/globnames.mli b/library/globnames.mli
index 8acea5ef28..58e0efbc7a 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -34,7 +34,6 @@ val destConstructRef : GlobRef.t -> constructor
 val is_global : GlobRef.t -> constr -> bool
 [@@ocaml.deprecated "Use [Constr.isRefX] instead."]
 
-val subst_constructor : substitution -> constructor -> constructor
 val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
-- 
cgit v1.2.3