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]

---
 kernel/mod_subst.ml  | 5 +++++
 kernel/mod_subst.mli | 3 +++
 2 files changed, 8 insertions(+)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c5ac57a2cd..d2fb773dc4 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -291,6 +291,11 @@ let subst_ind sub (ind,i as indi) =
   let ind' = subst_mind sub ind in
     if ind' == ind then indi else ind',i
 
+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_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 9cf270cff7..e7bfceb4de 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -127,6 +127,9 @@ val subst_mind :
 val subst_ind :
   substitution -> inductive -> inductive
 
+val subst_constructor :
+  substitution -> constructor -> constructor
+
 val subst_pind : substitution -> pinductive -> pinductive
 
 val subst_kn :
-- 
cgit v1.2.3