Names: shortcuts for building {kn, constant, mind} with empty sections

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

1 files changed, 6 insertions, 6 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index d07bacdf0..986118655 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -259,7 +259,7 @@ let add_retroknowledge mp =
 
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
-    let kn = make_kn mp DirPath.empty l in
+    let kn = KerName.make2 mp l in
     match elem with
       | SFBconst cb ->
 	Environ.add_constant (constant_of_delta_kn resolver kn) cb env
@@ -284,7 +284,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let kn = make_kn mp_from DirPath.empty l in
+      let kn = KerName.make2 mp_from l in
       let con = constant_of_delta_kn resolver kn in
       { cb with
 	const_body = Def (Declarations.from_val (mkConst con));
@@ -429,8 +429,8 @@ and strengthen_and_subst_struct
 	    (* If we are performing an inclusion we need to add
 	       the fact that the constant mp_to.l is \Delta-equivalent
 	       to resolver(mp_from.l) *)
-	  let kn_from = make_kn mp_from DirPath.empty l in
-	  let kn_to = make_kn mp_to DirPath.empty l in
+	  let kn_from = KerName.make2 mp_from l in
+	  let kn_to = KerName.make2 mp_to l in
 	  let old_name = kn_of_delta resolver kn_from in
 	  (add_kn_delta_resolver kn_to old_name resolve_out),
 	  item'::rest'
@@ -446,8 +446,8 @@ and strengthen_and_subst_struct
 	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	if incl then
-	  let kn_from = make_kn mp_from DirPath.empty l in
-	  let kn_to = make_kn mp_to DirPath.empty l in
+	  let kn_from = KerName.make2 mp_from l in
+	  let kn_to = KerName.make2 mp_to l in
 	  let old_name = kn_of_delta resolver kn_from in
 	  (add_kn_delta_resolver kn_to old_name resolve_out),
 	  item'::rest'