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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/mod_subst.mli')

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