diff options
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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) |