From 4bc680136b9310f7ab630e41b47314b9efdbe9d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Feb 2005 22:08:16 +0000
Subject: Moving subst_inductive from tacinterp to inductiveops for better for
 reuse in recordops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6741 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml  | 2 ++
 pretyping/inductiveops.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 74795f572c..a0b2cb80fc 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -369,3 +369,5 @@ let control_only_guard env =
     | LetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3
   in 
   control_rec 
+
+let subst_inductive subst (kn,i) = (Mod_subst.subst_kn subst kn,i)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7f18a79435..aa0306d2f5 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -99,3 +99,5 @@ val make_default_case_info : env -> case_style -> inductive -> case_info
 
 (********************)
 val control_only_guard : env -> types -> unit
+
+val subst_inductive : Mod_subst.substitution -> inductive -> inductive
-- 
cgit v1.2.3