Names: Modularize constant and mutual_inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 0 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 529f08cb1..2ff570a4a 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -223,6 +223,11 @@ let gen_subst_mp f sub mp1 mp2 =
     | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
     | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
 
+let make_mind_equiv mpu mpc dir l =
+  let knu = make_kn mpu dir l in
+  if mpu == mpc then mind_of_kn knu
+  else mind_of_kn_equiv knu (make_kn mpc dir l)
+
 let subst_ind sub mind =
   let kn1,kn2 = user_mind mind, canonical_mind mind in
   let mp1,dir,l = repr_kn kn1 in
@@ -235,6 +240,11 @@ let subst_ind sub mind =
       | Canonical -> mind_of_delta2 resolve mind'
   with No_subst -> mind
 
+let make_con_equiv mpu mpc dir l =
+  let knu = make_kn mpu dir l in
+  if mpu == mpc then constant_of_kn knu
+  else constant_of_kn_equiv knu (make_kn mpc dir l)
+
 let subst_con0 sub con =
   let kn1,kn2 = user_con con,canonical_con con in
   let mp1,dir,l = repr_kn kn1 in