Merge PR #8555: Remove section paths from kernel names

69 files changed, 269 insertions, 439 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 2f31ab1950..67e0e06caa 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -16,6 +16,9 @@ Plugins
 Tactics
 
 - Removed the deprecated `romega` tactics.
+- Tactic names are no longer allowed to clash, even if they are not defined in
+  the same section. For example, the following is no longer accepted:
+  `Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
 
 Changes from 8.8.2 to 8.9+beta1
 ===============================
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 03fee1ab51..93d5f8bfa2 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -70,12 +70,12 @@ let solve_delta_kn resolve kn =
       | Equiv kn1 -> kn1
       | Inline _ -> raise Not_found
   with Not_found ->
-    let mp,dir,l = KerName.repr kn in
+    let mp,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      KerName.make new_mp dir l
+      KerName.make new_mp l
 
 let gen_of_delta resolve x kn fix_can =
   let new_kn = solve_delta_kn resolve kn in
@@ -129,17 +129,17 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (KerName.make mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' l)
    | None -> kn
 
 let subst_kn sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      KerName.make mp' dir l
+      KerName.make mp' l
    | None -> kn
 
 exception No_subst
@@ -156,16 +156,16 @@ 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 = KerName.make mpu dir l in
+let make_mind_equiv mpu mpc l =
+  let knu = KerName.make mpu l in
   if mpu == mpc then MutInd.make1 knu
-  else MutInd.make knu (KerName.make mpc dir l)
+  else MutInd.make knu (KerName.make mpc l)
 
 let subst_ind sub mind =
   let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in
-  let mp1,dir,l = KerName.repr kn1 in
-  let mp2,_,_ = KerName.repr kn2 in
-  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+  let mp1,l = KerName.repr kn1 in
+  let mp2,_ = KerName.repr kn2 in
+  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 l in
   try
     let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
     match side with
@@ -173,16 +173,16 @@ 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 = KerName.make mpu dir l in
+let make_con_equiv mpu mpc l =
+  let knu = KerName.make mpu l in
   if mpu == mpc then Constant.make1 knu
-  else Constant.make knu (KerName.make mpc dir l)
+  else Constant.make knu (KerName.make mpc l)
 
 let subst_con0 sub con u =
   let kn1,kn2 = Constant.user con, Constant.canonical con in
-  let mp1,dir,l = KerName.repr kn1 in
-  let mp2,_,_ = KerName.repr kn2 in
-  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+  let mp1,l = KerName.repr kn1 in
+  let mp2,_ = KerName.repr kn2 in
+  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 l in
   let dup con = con, Const (con, u) in
   let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
   match constant_of_delta_with_inline resolve con' with
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 1fd86bc368..0478765a81 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -34,7 +34,7 @@ let string_of_mp mp =
   if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
 
 let prkn kn =
-  let (mp,_,l) = KerName.repr kn in
+  let (mp,l) = KerName.repr kn in
   str(string_of_mp mp ^ "." ^ Label.to_string l)
 let prcon c =
   let ck = Constant.canonical c in
diff --git a/checker/modops.ml b/checker/modops.ml
index b92d7bbf1f..541d009ff9 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -55,7 +55,7 @@ let module_body_of_type mp mtb =
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
-    let kn = KerName.make2 mp l in
+    let kn = KerName.make mp l in
     let con = Constant.make1 kn in
     let mind = mind_of_delta resolver (MutInd.make1 kn) in
       match elem with
diff --git a/checker/values.ml b/checker/values.ml
index 35027d5bfb..24f10b7a87 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -98,7 +98,7 @@ let rec v_mp = Sum("module_path",0,
   [|[|v_dp|];
     [|v_uid|];
     [|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_id;Int|]
 let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
 let v_ind = v_tuple "inductive" [|v_cst;Int|]
 let v_cons = v_tuple "constructor" [|v_ind;Int|]
diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
new file mode 100644
index 0000000000..41c2ad6fef
--- /dev/null
+++ b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then
+
+    ltac2_CI_REF=rm-section-path
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    Equations_CI_REF=rm-section-path
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9d592ee879..d6d296f012 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,18 @@
 ## Changes between Coq 8.9 and Coq 8.10
 
+### ML API
+
+Names
+
+- Kernel names no longer contain a section path. They now have only two
+  components (module path and label), which led to some changes in the API:
+
+  KerName.make takes only 2 components
+  KerName.repr returns only 2 components
+  KerName.make2 is now KerName.make
+  Constant.make3 has been removed, use Constant.make2
+  Constant.repr3 has been removed, use Constant.repr2
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e15fd776b2..8129a4a867 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -552,23 +552,22 @@ open Libnames
 let encode_path ?loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
-    | Some (mp,dir) ->
-	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
-	DirPath.repr dir) in
+    | Some mp -> DirPath.repr (dirpath_of_string (ModPath.to_string mp))
+  in
   make_qualid ?loc
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
-      let (mp,dir,id) = Constant.repr3 cst in
-      encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id)
+      let (mp,id) = Constant.repr2 cst in
+      encode_path ?loc "CST" (Some mp) [] (Label.to_id id)
   | IndRef (kn,i) ->
-      let (mp,dir,id) = MutInd.repr3 kn in
-      encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id]
+      let (mp,id) = MutInd.repr2 kn in
+      encode_path ?loc "IND" (Some mp) [Label.to_id id]
 	(Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
-      let (mp,dir,id) = MutInd.repr3 kn in
-      encode_path ?loc "CSTR" (Some (mp,dir))
+      let (mp,id) = MutInd.repr2 kn in
+      encode_path ?loc "CSTR" (Some mp)
 	[Label.to_id id;Id.of_string ("_"^string_of_int i)]
 	(Id.of_string ("_"^string_of_int j))
   | VarRef id ->
@@ -576,14 +575,14 @@ let raw_string_of_ref ?loc _ = function
 
 let short_string_of_ref ?loc _ = function
   | VarRef id -> qualid_of_ident ?loc id
-  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn))
   | IndRef (kn,i) ->
-      encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
+      encode_path ?loc "IND" None [Label.to_id (MutInd.label kn)]
         (Id.of_string ("_"^string_of_int i))
   | ConstructRef ((kn,i),j) ->
       encode_path ?loc "CSTR" None
-        [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)]
+        [Label.to_id (MutInd.label kn);Id.of_string ("_"^string_of_int i)]
         (Id.of_string ("_"^string_of_int j))
 
 (* Anticipate that printers can be used from ocamldebug and that 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 2a59b914db..7ce759a3fb 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -76,9 +76,9 @@ let is_imported_ref = function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
-      let (mp,_,_) = MutInd.repr3 kn in is_imported_modpath mp
+      let mp = MutInd.modpath kn in is_imported_modpath mp
   | ConstRef kn ->
-      let (mp,_,_) = Constant.repr3 kn in is_imported_modpath mp
+      let mp = Constant.modpath kn in is_imported_modpath mp
 
 let is_global id =
   try
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 70cdd3a2db..e89dcedb9c 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -69,7 +69,7 @@ let discharge_ubinder (_,(ref,l)) =
       with Not_found -> name_universe lvl
   in
   let l = List.map map sec_inst @ l in
-  Some (Lib.discharge_global ref, l)
+  Some (ref, l)
 
 let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
   let open Libobject in
diff --git a/interp/declare.ml b/interp/declare.ml
index 23c68b5e18..f4e57073cc 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -78,7 +78,6 @@ let check_exists sp =
 
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
-  let _,dir,_ = KerName.repr kn in
   let kn' =
     match obj.cst_decl with
     | None ->
@@ -87,7 +86,7 @@ let cache_constant ((sp,kn), obj) =
       else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     | Some decl ->
       let () = check_exists sp in
-      Global.add_constant dir id decl
+      Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl
   in
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
@@ -136,7 +135,7 @@ let register_side_effect (c, role) =
     cst_kind = IsProof Theorem;
     cst_locl = false;
   } in
-  let id = Label.to_id (pi3 (Constant.repr3 c)) in
+  let id = Label.to_id (Constant.label c) in
   ignore(add_leaf id o);
   update_tables c;
   match role with
@@ -311,8 +310,7 @@ let cache_inductive ((sp,kn),mie) =
   let names = inductive_names sp kn mie in
   List.iter check_exists (List.map fst names);
   let id = basename sp in
-  let _,dir,_ = KerName.repr kn in
-  let kn' = Global.add_mind dir id mie in
+  let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
   add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index ccad6b19eb..f5be0ddbae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -234,7 +234,7 @@ let add_glob ?loc ref =
     add_glob_gen ?loc sp lib_dp ty
 
 let mp_of_kn kn =
-  let mp,sec,l = Names.KerName.repr kn in
+  let mp,l = Names.KerName.repr kn in
     Names.MPdot (mp,l)
 
 let add_glob_kn ?loc kn =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 3603367cf1..ce33cb8731 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -561,29 +561,27 @@ let discharge_implicits (_,(req,l)) =
   | ImplInteractive (ref,flags,exp) ->
     (try
       let vars = variable_section_segment_of_reference ref in
-      let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
-      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
-      Some (ImplInteractive (ref',flags,exp),l')
+      let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      Some (ImplInteractive (ref,flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
     (try
-      let con' = pop_con con in
       let vars = variable_section_segment_of_reference (ConstRef con) in
       let extra_impls = impls_of_context vars in
       let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
-      let l' = [ConstRef con',newimpls] in
-	Some (ImplConstant (con',flags),l')
+      let l' = [ConstRef con,newimpls] in
+        Some (ImplConstant (con,flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
 	let vars = variable_section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
-	((if isVarRef gr then gr else pop_global_reference gr),
+        (gr,
 	 List.map (add_section_impls vars extra_impls) l)) l
       in
-	Some (ImplMutualInductive (pop_kn kn,flags),l')
+        Some (ImplMutualInductive (kn,flags),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
 
 let rebuild_implicits (req,l) =
diff --git a/interp/notation.ml b/interp/notation.ml
index 02c7812e21..6104ab16c7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1304,7 +1304,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
         vars |> List.map fst |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
-    Some (req,Lib.discharge_global r,n,l,[])
+    Some (req,r,n,l,[])
 
 let classify_arguments_scope (req,_,_,_,_ as obj) =
   if req == ArgsScopeNoDischarge then Dispose else Substitute obj
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b361e36bbf..b39aed01e8 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -15,7 +15,6 @@
 (* This module implements kernel-level discharching of local
    declarations over global constants and inductive types *)
 
-open CErrors
 open Util
 open Names
 open Term
@@ -28,18 +27,6 @@ module RelDecl = Context.Rel.Declaration
 
 (*s Cooking the constants. *)
 
-let pop_dirpath p = match DirPath.repr p with
-  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
-  | _::l -> DirPath.make l
-
-let pop_mind kn =
-  let (mp,dir,l) = MutInd.repr3 kn in
-  MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_con con =
-  let (mp,dir,l) = Constant.repr3 con in
-  Constant.make3 mp (pop_dirpath dir) l
-
 type my_global_reference =
   | ConstRef of Constant.t
   | IndRef of inductive
@@ -71,29 +58,26 @@ let instantiate_my_gr gr u =
 let share cache r (cstl,knl) =
   try RefTable.find cache r
   with Not_found ->
-  let f,(u,l) =
+  let (u,l) =
     match r with
-    | IndRef (kn,i) ->
-	IndRef (pop_mind kn,i), Mindmap.find kn knl
-    | ConstructRef ((kn,i),j) ->
-	ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
+    | IndRef (kn,_i) ->
+        Mindmap.find kn knl
+    | ConstructRef ((kn,_i),_j) ->
+        Mindmap.find kn knl
     | ConstRef cst ->
-	ConstRef (pop_con cst), Cmap.find cst cstl in
-  let c = (f, (u, Array.map mkVar l)) in
+        Cmap.find cst cstl in
+  let c = (u, Array.map mkVar l) in
   RefTable.add cache r c;
   c
 
 let share_univs cache r u l =
-  let r', (u', args) = share cache r l in
-    mkApp (instantiate_my_gr r' (Instance.append u' u), args)
+  let (u', args) = share cache r l in
+    mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
 let update_case_info cache ci modlist =
   try
-    let ind, n =
-      match share cache (IndRef ci.ci_ind) modlist with
-      | (IndRef f,(_u,l)) -> (f, Array.length l)
-      | _ -> assert false in
-    { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
+    let (_u,l) = share cache (IndRef ci.ci_ind) modlist in
+    { ci with ci_npar = ci.ci_npar + Array.length l }
   with Not_found ->
     ci
 
@@ -129,7 +113,7 @@ let expmod_constr cache modlist c =
       | Proj (p, c') ->
         let map cst npars =
           let _, newpars = Mindmap.find cst (snd modlist) in
-          pop_mind cst, npars + Array.length newpars
+          (cst, npars + Array.length newpars)
         in
         let p' = try Projection.map_npars map p with Not_found -> p in
         let c'' = substrec c' in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index bff3092655..2a91c7dab0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -173,12 +173,12 @@ let solve_delta_kn resolve kn =
       | Inline (lev, Some c) ->	raise (Change_equiv_to_inline (lev,c))
       | Inline (_, None) -> raise Not_found
   with Not_found ->
-    let mp,dir,l = KerName.repr kn in
+    let mp,l = KerName.repr kn in
     let new_mp = find_prefix resolve mp in
     if mp == new_mp then
       kn
     else
-      KerName.make new_mp dir l
+      KerName.make new_mp l
 
 let kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
@@ -245,18 +245,18 @@ let subst_mp sub mp =
   | Some (mp',_) -> mp'
 
 let subst_kn_delta sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',resolve) ->
-      solve_delta_kn resolve (KerName.make mp' dir l)
+      solve_delta_kn resolve (KerName.make mp' l)
    | None -> kn
 
 
 let subst_kn sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   match subst_mp0 sub mp with
      Some (mp',_) ->
-      (KerName.make mp' dir l)
+      (KerName.make mp' l)
    | None -> kn
 
 exception No_subst
@@ -275,12 +275,12 @@ let progress f x ~orelse =
   if y != x then y else orelse
 
 let subst_mind sub mind =
-  let mpu,dir,l = MutInd.repr3 mind in
+  let mpu,l = MutInd.repr2 mind in
   let mpc = KerName.modpath (MutInd.canonical mind) in
   try
     let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
-    let knu = KerName.make mpu dir l in
-    let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+    let knu = KerName.make mpu l in
+    let knc = if mpu == mpc then knu else KerName.make mpc l in
     let knc' =
       progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
     in
@@ -295,11 +295,11 @@ let subst_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
 let subst_con0 sub (cst,u) =
-  let mpu,dir,l = Constant.repr3 cst in
+  let mpu,l = Constant.repr2 cst in
   let mpc = KerName.modpath (Constant.canonical cst) in
   let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
-  let knu = KerName.make mpu dir l in
-  let knc = if mpu == mpc then knu else KerName.make mpc dir l in
+  let knu = KerName.make mpu l in
+  let knc = if mpu == mpc then knu else KerName.make mpc l in
   match search_delta_inline resolve knu knc with
     | Some (ctx, t) ->
       (* In case of inlining, discard the canonical part (cf #2608) *)
@@ -433,10 +433,10 @@ let rec replace_mp_in_mp mpfrom mpto mp =
     | _ -> mp
 
 let replace_mp_in_kn mpfrom mpto kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
   let mp'' = replace_mp_in_mp mpfrom mpto mp in
     if mp==mp'' then kn
-    else KerName.make mp'' dir l
+    else KerName.make mp'' l
 
 let rec mp_in_mp mp mp1 =
   match mp1 with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 424d329e09..bab2eae3df 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -289,10 +289,10 @@ let add_retroknowledge =
 let rec add_structure mp sign resolver linkinfo env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
-      let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
+      let c = constant_of_delta_kn resolver (KerName.make mp l) in
       Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
-      let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
+      let mind = mind_of_delta_kn resolver (KerName.make mp l) in
       let mib = 
 	if mib.mind_private != None then 
 	  { mib with mind_private = Some true }
@@ -331,7 +331,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
   |Def _ -> cb
   |_ ->
-    let kn = KerName.make2 mp_from l in
+    let kn = KerName.make mp_from l in
     let con = constant_of_delta_kn resolver kn in
     let u =
       match cb.const_universes with
@@ -450,8 +450,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
           (* If we are performing an inclusion we need to add
              the fact that the constant mp_to.l is \Delta-equivalent
              to reso(mp_from.l) *)
-          let kn_from = KerName.make2 mp_from l in
-          let kn_to = KerName.make2 mp_to l in
+          let kn_from = KerName.make mp_from l in
+          let kn_to = KerName.make mp_to l in
           let old_name = kn_of_delta reso kn_from in
 	  add_kn_delta_resolver kn_to old_name reso', str'
 	else
@@ -471,8 +471,8 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
         in
 	(* Same as constant *)
 	if incl then
-	  let kn_from = KerName.make2 mp_from l in
-	  let kn_to = KerName.make2 mp_to l in
+          let kn_from = KerName.make mp_from l in
+          let kn_to = KerName.make mp_to l in
 	  let old_name = kn_of_delta reso kn_from in
           add_kn_delta_resolver kn_to old_name reso', str'
 	else
diff --git a/kernel/names.ml b/kernel/names.ml
index 6d33f233e9..1e28ec51fb 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -365,7 +365,6 @@ module KerName = struct
 
   type t = {
     modpath : ModPath.t;
-    dirpath : DirPath.t;
     knlabel : Label.t;
     mutable refhash : int;
     (** Lazily computed hash. If unset, it is set to negative values. *)
@@ -373,22 +372,18 @@ module KerName = struct
 
   type kernel_name = t
 
-  let make modpath dirpath knlabel =
-    { modpath; dirpath; knlabel; refhash = -1; }
-  let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
+  let make modpath knlabel =
+    { modpath; knlabel; refhash = -1; }
+  let repr kn = (kn.modpath, kn.knlabel)
 
-  let make2 modpath knlabel =
-    { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
+  let make2 = make
+  [@@ocaml.deprecated "Please use [KerName.make]"]
 
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
   let to_string_gen mp_to_string kn =
-    let dp =
-      if DirPath.is_empty kn.dirpath then "."
-      else "#" ^ DirPath.to_string kn.dirpath ^ "#"
-    in
-    mp_to_string kn.modpath ^ dp ^ Label.to_string kn.knlabel
+    mp_to_string kn.modpath ^ "." ^ Label.to_string kn.knlabel
 
   let to_string kn = to_string_gen ModPath.to_string kn
 
@@ -402,9 +397,7 @@ module KerName = struct
       let c = String.compare kn1.knlabel kn2.knlabel in
       if not (Int.equal c 0) then c
       else
-        let c = DirPath.compare kn1.dirpath kn2.dirpath in
-        if not (Int.equal c 0) then c
-        else ModPath.compare kn1.modpath kn2.modpath
+        ModPath.compare kn1.modpath kn2.modpath
 
   let equal kn1 kn2 =
     let h1 = kn1.refhash in
@@ -412,7 +405,6 @@ module KerName = struct
     if 0 <= h1 && 0 <= h2 && not (Int.equal h1 h2) then false
     else
       Label.equal kn1.knlabel kn2.knlabel &&
-      DirPath.equal kn1.dirpath kn2.dirpath &&
       ModPath.equal kn1.modpath kn2.modpath
 
   open Hashset.Combine
@@ -420,8 +412,8 @@ module KerName = struct
   let hash kn =
     let h = kn.refhash in
     if h < 0 then
-      let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in
-      let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in
+      let { modpath = mp; knlabel = lbl; _ } = kn in
+      let h = combine (ModPath.hash mp) (Label.hash lbl) in
       (* Ensure positivity on all platforms. *)
       let h = h land 0x3FFFFFFF in
       let () = kn.refhash <- h in
@@ -432,12 +424,11 @@ module KerName = struct
     type t = kernel_name
     type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
         * (string -> string)
-    let hashcons (hmod,hdir,hstr) kn =
-      let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
-      { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
+    let hashcons (hmod,_hdir,hstr) kn =
+      let { modpath = mp; knlabel = l; refhash; } = kn in
+      { modpath = hmod mp; knlabel = hstr l; refhash; }
     let eq kn1 kn2 =
-      kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
-        kn1.knlabel == kn2.knlabel
+      kn1.modpath == kn2.modpath && kn1.knlabel == kn2.knlabel
     let hash = hash
   end
 
@@ -492,21 +483,20 @@ module KerPair = struct
   let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
 
   let make1 = same
-  let make2 mp l = same (KerName.make2 mp l)
-  let make3 mp dir l = same (KerName.make mp dir l)
-  let repr3 kp = KerName.repr (user kp)
+  let make2 mp l = same (KerName.make mp l)
+  let repr2 kp = KerName.repr (user kp)
   let label kp = KerName.label (user kp)
   let modpath kp = KerName.modpath (user kp)
 
   let change_label kp lbl =
-    let (mp1,dp1,l1) = KerName.repr (user kp)
-    and (mp2,dp2,l2) = KerName.repr (canonical kp) in
-    assert (String.equal l1 l2 && DirPath.equal dp1 dp2);
+    let (mp1,l1) = KerName.repr (user kp)
+    and (mp2,l2) = KerName.repr (canonical kp) in
+    assert (String.equal l1 l2);
     if String.equal lbl l1 then kp
     else
-      let kn = KerName.make mp1 dp1 lbl in
+      let kn = KerName.make mp1 lbl in
       if mp1 == mp2 then same kn
-      else make kn (KerName.make mp2 dp2 lbl)
+      else make kn (KerName.make mp2 lbl)
 
   let to_string kp = KerName.to_string (user kp)
   let print kp = str (to_string kp)
diff --git a/kernel/names.mli b/kernel/names.mli
index 2ea8108734..2145a51c4e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -274,9 +274,11 @@ sig
   type t
 
   (** Constructor and destructor *)
-  val make : ModPath.t -> DirPath.t -> Label.t -> t
+  val make : ModPath.t -> Label.t -> t
+  val repr : t -> ModPath.t * Label.t
+
   val make2 : ModPath.t -> Label.t -> t
-  val repr : t -> ModPath.t * DirPath.t * Label.t
+  [@@ocaml.deprecated "Please use [KerName.make]"]
 
   (** Projections *)
   val modpath : t -> ModPath.t
@@ -317,15 +319,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
@@ -403,15 +402,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 74b075f4a5..482a2f3a3c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function
 let list_of_mp mp = list_of_mp [] mp
 
 let string_of_kn kn =
-  let (mp,_dp,l) = KerName.repr kn in
+  let (mp,l) = KerName.repr kn in
   let mp = list_of_mp mp in
   String.concat "_" mp ^ "_" ^ string_of_label l
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 8ac3538fc5..5d1b882361 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -27,7 +27,7 @@ let rec translate_mod prefix mp env mod_expr acc =
 and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
-     let con = Constant.make3 mp DirPath.empty l in
+     let con = Constant.make2 mp l in
      (if !Flags.debug then
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
 	Feedback.msg_debug (Pp.str msg));
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b036aa6a67..b03342da39 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -479,10 +479,10 @@ type global_declaration =
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
 
-let add_constant_aux no_section senv (kn, cb) =
-  let l = pi3 (Constant.repr3 kn) in
+let add_constant_aux ~in_section senv (kn, cb) =
+  let l = Constant.label kn in
   let cb, otab = match cb.const_body with
-    | OpaqueDef lc when no_section ->
+    | OpaqueDef lc when not in_section ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       let od, otab =
@@ -505,13 +505,11 @@ let export_private_constants ~in_section ce senv =
   let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
   let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
-  let no_section = not in_section in
-  let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+  let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_constant dir l decl senv =
-  let kn = Constant.make3 senv.modpath dir l in
-  let no_section = DirPath.is_empty dir in
+let add_constant ~in_section l decl senv =
+  let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
       match decl with
@@ -520,9 +518,9 @@ let add_constant dir l decl senv =
       | ConstantEntry (PureEntry, ce) ->
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
       | GlobalRecipe r ->
-        let cb = Term_typing.translate_recipe senv.env kn r in
-        if no_section then Declareops.hcons_const_body cb else cb in
-    add_constant_aux no_section senv (kn, cb) in
+        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+        if in_section then cb else Declareops.hcons_const_body cb in
+    add_constant_aux ~in_section senv (kn, cb) in
   kn, senv
 
 (** Insertion of inductive types *)
@@ -535,9 +533,9 @@ let check_mind mie lab =
     (* The label and the first inductive type name should match *)
     assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
 
-let add_mind dir l mie senv =
+let add_mind l mie senv =
   let () = check_mind mie l in
-  let kn = MutInd.make3 senv.modpath dir l in
+  let kn = MutInd.make2 senv.modpath l in
   let mib = Term_typing.translate_mind senv.env kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
@@ -770,9 +768,9 @@ let add_include me is_module inl senv =
   let add senv ((l,elem) as field) =
     let new_name = match elem with
       | SFBconst _ ->
-        C (Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp_sup l))
+        C (Mod_subst.constant_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmind _ ->
-	I (Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp_sup l))
+        I (Mod_subst.mind_of_delta_kn resolver (KerName.make mp_sup l))
       | SFBmodule _ -> M
       | SFBmodtype _ -> MT
     in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6e0febaa3f..efb4957006 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -105,13 +105,13 @@ val export_private_constants : in_section:bool ->
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
 val add_constant :
-  DirPath.t -> Label.t -> global_declaration ->
+  in_section:bool -> Label.t -> global_declaration ->
     Constant.t safe_transformer
 
 (** Adding an inductive type *)
 
 val add_mind :
-  DirPath.t -> Label.t -> Entries.mutual_inductive_entry ->
+  Label.t -> Entries.mutual_inductive_entry ->
     MutInd.t safe_transformer
 
 (** Adding a module or a module type *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bfe68671a2..d64342dbb0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,8 @@ let check_polymorphic_instance error env auctx1 auctx2 =
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
-  let kn1 = KerName.make2 mp1 l in
-  let kn2 = KerName.make2 mp2 l in
+  let kn1 = KerName.make mp1 l in
+  let kn2 = KerName.make mp2 l in
   let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 47247ff25e..5ccc23eefc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -531,11 +531,7 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     t
 
-let translate_recipe env kn r =
-  (** We only hashcons the term when outside of a section, otherwise this would
-      be useless. It is detected by the dirpath of the constant being empty. *)
-  let (_, dir, _) = Constant.repr3 kn in
-  let hcons = DirPath.is_empty dir in
+let translate_recipe ~hcons env kn r =
   build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
 
 let translate_local_def env _id centry =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b05e05e4dc..ab25090b00 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -64,7 +64,7 @@ val export_side_effects :
 val translate_mind :
   env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 026b7aa316..e71de4d77e 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -119,29 +119,26 @@ let prelude_module_name = init_dir@["Prelude"]
 let prelude_module = make_dir prelude_module_name
 
 let logic_module_name = init_dir@["Logic"]
-let logic_module = make_dir logic_module_name
+let logic_module = MPfile (make_dir logic_module_name)
 
 let logic_type_module_name = init_dir@["Logic_Type"]
 let logic_type_module = make_dir logic_type_module_name
 
 let datatypes_module_name = init_dir@["Datatypes"]
-let datatypes_module = make_dir datatypes_module_name
+let datatypes_module = MPfile (make_dir datatypes_module_name)
 
 let jmeq_module_name = [coq;"Logic";"JMeq"]
-let jmeq_module = make_dir jmeq_module_name
-
-(* TODO: temporary hack. Works only if the module isn't an alias *)
-let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
-let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+let jmeq_library_path = make_dir jmeq_module_name
+let jmeq_module = MPfile jmeq_library_path
 
 (** Identity *)
 
-let id = make_con datatypes_module "idProp"
-let type_of_id = make_con datatypes_module "IDProp"
+let id = Constant.make2 datatypes_module @@ Label.make "idProp"
+let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
 
 (** Natural numbers *)
-let nat_kn = make_ind datatypes_module "nat"
-let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat"
+let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat")
 
 let glob_nat = IndRef (nat_kn,0)
 
@@ -151,7 +148,7 @@ let glob_O = ConstructRef path_of_O
 let glob_S = ConstructRef path_of_S
 
 (** Booleans *)
-let bool_kn = make_ind datatypes_module "bool"
+let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
 
 let glob_bool = IndRef (bool_kn,0)
 
@@ -161,13 +158,13 @@ let glob_true  = ConstructRef path_of_true
 let glob_false  = ConstructRef path_of_false
 
 (** Equality *)
-let eq_kn = make_ind logic_module "eq"
+let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
 let glob_eq = IndRef (eq_kn,0)
 
-let identity_kn = make_ind datatypes_module "identity"
+let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
 let glob_identity = IndRef (identity_kn,0)
 
-let jmeq_kn = make_ind jmeq_module "JMeq"
+let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
 let glob_jmeq = IndRef (jmeq_kn,0)
 
 type coq_sigma_data = {
diff --git a/library/coqlib.mli b/library/coqlib.mli
index 8844684957..6a3d0953cd 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -61,12 +61,13 @@ val init_modules : string list list
 (** Modules *)
 val prelude_module : DirPath.t
 
-val logic_module : DirPath.t
+val logic_module : ModPath.t
 val logic_module_name : string list
 
 val logic_type_module : DirPath.t
 
-val jmeq_module : DirPath.t
+val jmeq_module : ModPath.t
+val jmeq_library_path : DirPath.t
 val jmeq_module_name : string list
 
 val datatypes_module_name : string list
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0b3b461e6c..e01a99f731 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -164,8 +164,7 @@ module ModObjs :
 *)
 
 let mp_of_kn kn =
-  let mp,sec,l = KerName.repr kn in
-  assert (DirPath.is_empty sec);
+  let mp,l = KerName.repr kn in
   MPdot (mp,l)
 
 let dir_of_sp sp =
diff --git a/library/global.ml b/library/global.ml
index e872d081d6..0e236e6d34 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -91,8 +91,8 @@ let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
-let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
-let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
+let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
+let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 5205968c7b..fd6c9a60d4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -42,9 +42,9 @@ val export_private_constants : in_section:bool ->
   unit Entries.definition_entry * Safe_typing.exported_private_constant list
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t
+  in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_mind :
-  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t
+  Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
 val add_constraints : Univ.Constraint.t -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index 6bbdd36489..9aca7788d2 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -8,11 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Names
 open Constr
 open Mod_subst
-open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
 type global_reference = GlobRef.t =
@@ -137,53 +135,5 @@ type global_reference_or_constr =
   | IsGlobal of global_reference
   | IsConstr of constr
 
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id)
-
-let encode_con dir id = Constant.make2 (MPfile dir) (Label.of_id id)
-
-let check_empty_section dp =
-  if not (DirPath.is_empty dp) then
-    anomaly (Pp.str "Section part should be empty!")
-
-let decode_mind kn =
-  let rec dir_of_mp = function
-    | MPfile dir -> DirPath.repr dir
-    | MPbound mbid ->
-	let _,_,dp = MBId.repr mbid in
-	let id = MBId.to_id mbid in
-	  id::(DirPath.repr dp)
-    | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
-  in
-  let mp,sec_dir,l = MutInd.repr3 kn in
-  check_empty_section sec_dir;
-  (DirPath.make (dir_of_mp mp)),Label.to_id l
-
-let decode_con kn =
-  let mp,sec_dir,l = Constant.repr3 kn in
-  check_empty_section sec_dir;
-  match mp with
-    | MPfile dir -> (dir,Label.to_id l)
-    | _ -> anomaly (Pp.str "MPfile expected!")
-
-(** Popping one level of section in global names.
-    These functions are meant to be used during discharge:
-    user and canonical kernel names must be equal. *)
-
-let pop_con con =
-  let (mp,dir,l) = Constant.repr3 con in
-  Constant.make3 mp (pop_dirpath dir) l
-
-let pop_kn kn =
-  let (mp,dir,l) = MutInd.repr3 kn in
-  MutInd.make3 mp (pop_dirpath dir) l
-
-let pop_global_reference = function
-  | ConstRef con -> ConstRef (pop_con con)
-  | IndRef (kn,i) -> IndRef (pop_kn kn,i)
-  | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
-  | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
-
 (* Deprecated *)
 let eq_gr = GlobRef.equal
diff --git a/library/globnames.mli b/library/globnames.mli
index 45ee069b06..a96a42ced2 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -82,15 +82,3 @@ end
 type global_reference_or_constr = 
   | IsGlobal of GlobRef.t
   | IsConstr of constr
-
-(** {6 Temporary function to brutally form kernel names from section paths } *)
-
-val encode_mind : DirPath.t -> Id.t -> MutInd.t
-val decode_mind : MutInd.t -> DirPath.t * Id.t
-val encode_con : DirPath.t -> Id.t -> Constant.t
-val decode_con : Constant.t -> DirPath.t * Id.t
-
-(** {6 Popping one level of section in global names } *)
-val pop_con : Constant.t -> Constant.t
-val pop_kn : MutInd.t-> MutInd.t
-val pop_global_reference : GlobRef.t -> GlobRef.t
diff --git a/library/keys.ml b/library/keys.ml
index a74d13c600..53447a679a 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -92,8 +92,7 @@ let subst_keys (subst,(k,k')) =
   (subst_key subst k, subst_key subst k')
 
 let discharge_key = function
-  | KGlob g when Lib.is_in_section g ->
-    if isVarRef g then None else Some (KGlob (pop_global_reference g))
+  | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
diff --git a/library/lib.ml b/library/lib.ml
index 07026a9c2a..27c5056a7f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -135,8 +135,8 @@ let make_path_except_section id =
   Libnames.make_path (cwd_except_section ()) id
 
 let make_kn id =
-  let mp, dir = current_mp (), current_sections () in
-  Names.KerName.make mp dir (Names.Label.of_id id)
+  let mp = current_mp () in
+  Names.KerName.make mp (Names.Label.of_id id)
 
 let make_oname id = Libnames.make_oname !lib_state.path_prefix id
 
@@ -632,44 +632,12 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-(************************)
-(* Discharging names *)
-
-let con_defined_in_sec kn =
-  let _,dir,_ = Names.Constant.repr3 kn in
-  not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let defined_in_sec kn =
-  let _,dir,_ = Names.MutInd.repr3 kn in
-  not (Names.DirPath.is_empty dir) &&
-  Names.DirPath.equal (pop_dirpath dir) (current_sections ())
-
-let discharge_global = function
-  | ConstRef kn when con_defined_in_sec kn ->
-      ConstRef (Globnames.pop_con kn)
-  | IndRef (kn,i) when defined_in_sec kn ->
-      IndRef (Globnames.pop_kn kn,i)
-  | ConstructRef ((kn,i),j) when defined_in_sec kn ->
-      ConstructRef ((Globnames.pop_kn kn,i),j)
-  | r -> r
-
-let discharge_kn kn =
-  if defined_in_sec kn then Globnames.pop_kn kn else kn
-
-let discharge_con cst =
-  if con_defined_in_sec cst then Globnames.pop_con cst else cst
-
 let discharge_proj_repr =
   Projection.Repr.map_npars (fun mind npars ->
-      if not (defined_in_sec mind) then mind, npars
-      else
-        let modlist = replacement_context () in
-        let _, newpars = Mindmap.find mind (snd modlist) in
-        Globnames.pop_kn mind, npars + Array.length newpars)
-
-let discharge_inductive (kn,i) =
-  (discharge_kn kn,i)
+      if not (is_in_section (IndRef (mind,0))) then mind, npars
+      else let modlist = replacement_context () in
+      let _, newpars = Mindmap.find mind (snd modlist) in
+      mind, npars + Array.length newpars)
 
 let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
   let open Univ in
diff --git a/library/lib.mli b/library/lib.mli
index a7d21060e9..686e6a0e2d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -187,10 +187,8 @@ val is_polymorphic_univ : Univ.Level.t -> bool
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
-val discharge_kn :  MutInd.t -> MutInd.t
-val discharge_con : Constant.t -> Constant.t
+(* XXX Why can't we use the kernel functions ? *)
+
 val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t
-val discharge_global : GlobRef.t -> GlobRef.t
-val discharge_inductive : inductive -> inductive
 val discharge_abstract_universe_context :
   abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
diff --git a/library/libnames.ml b/library/libnames.ml
index 23085048a1..bd2ca550b9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -171,8 +171,8 @@ type object_prefix = {
 }
 
 (* let make_oname (dirpath,(mp,dir)) id = *)
-let make_oname { obj_dir; obj_mp; obj_sec } id =
-  make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id)
+let make_oname { obj_dir; obj_mp } id =
+  make_path obj_dir id, KerName.make obj_mp (Label.of_id id)
 
 (* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index d413cd1e6d..bdeb6fca60 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -588,7 +588,7 @@ let pp_global k r =
   let ls = ref_renaming (k,r) in
   assert (List.length ls > 1);
   let s = List.hd ls in
-  let mp,_,l = repr_of_r r in
+  let mp,l = repr_of_r r in
   if ModPath.equal mp (top_visible_mp ()) then
     (* simpliest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5d3115d8d7..b0f6301192 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,7 +30,7 @@ open Common
 let toplevel_env () =
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
-	let mp,_,l = KerName.repr kn in
+        let mp,l = KerName.repr kn in
 	begin match Libobject.object_tag o with
 	  | "CONSTANT" ->
             let constant = Global.lookup_constant (Constant.make1 kn) in
@@ -124,7 +124,7 @@ module Visit : VISIT = struct
 end
 
 let add_field_label mp = function
-  | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
+  | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make mp lab)
   | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
 
 let rec add_labels mp = function
@@ -208,10 +208,10 @@ let env_for_mtb_with_def env mp me reso idl =
   Modops.add_structure mp before reso env
 
 let make_cst resolver mp l =
-  Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+  Mod_subst.constant_of_delta_kn resolver (KerName.make mp l)
 
 let make_mind resolver mp l =
-  Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
+  Mod_subst.mind_of_delta_kn resolver (KerName.make mp l)
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6ee1770a4e..7b4fd280bd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -36,16 +36,16 @@ let occur_kn_in_ref kn = function
   | ConstRef _ | VarRef _ -> false
 
 let repr_of_r = function
-  | ConstRef kn -> Constant.repr3 kn
+  | ConstRef kn -> Constant.repr2 kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+  | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
   | VarRef v -> KerName.repr (Lib.make_kn v)
 
 let modpath_of_r r =
-  let mp,_,_ = repr_of_r r in mp
+  let mp,_ = repr_of_r r in mp
 
 let label_of_r r =
-  let _,_,l = repr_of_r r in l
+  let _,l = repr_of_r r in l
 
 let rec base_mp = function
   | MPdot (mp,l) -> base_mp mp
@@ -95,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
 
 let labels_of_ref r =
   let mp_top = Lib.current_mp () in
-  let mp,_,l = repr_of_r r in
+  let mp,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
 
@@ -189,7 +189,7 @@ let init_recursors () = recursors := KNset.empty
 let add_recursors env ind =
   let kn = MutInd.canonical ind in
   let mk_kn id =
-    KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
+    KerName.make (KerName.modpath kn) (Label.of_id id)
   in
   let mib = Environ.lookup_mind ind env in
   Array.iter
@@ -287,7 +287,7 @@ let safe_pr_long_global r =
   try Printer.pr_global r
   with Not_found -> match r with
     | ConstRef kn ->
-	let mp,_,l = Constant.repr3 kn in
+        let mp,l = Constant.repr2 kn in
 	str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
 
@@ -653,8 +653,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        classify_function = (fun o -> Substitute o);
-       discharge_function =
-	(fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
+       discharge_function = (fun (_,x) -> Some x);
        subst_function =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a8baeaf1b6..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
 
 val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val repr_of_r : GlobRef.t -> ModPath.t * Label.t
 val modpath_of_r : GlobRef.t -> ModPath.t
 val label_of_r : GlobRef.t -> Label.t
 val base_mp : ModPath.t -> ModPath.t
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b2a528a1fd..839915631d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -394,7 +394,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 
 exception Not_Rec
 
-let get_funs_constant mp dp =
+let get_funs_constant mp =
   let get_funs_constant const e : (Names.Constant.t*int) array =
     match Constr.kind ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
@@ -402,7 +402,7 @@ let get_funs_constant mp dp =
 	    (fun i na ->
 	       match na with
 		 | Name id ->
-		     let const = Constant.make3 mp dp (Label.of_id id) in
+                     let const = Constant.make2 mp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
 		     anomaly (Pp.str "Anonymous fix.")
@@ -474,13 +474,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
-  let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
+  let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
   let first_fun_kn =
     try
       fst (find_Function_infos  (fst first_fun)).graph_ind
     with Not_found -> raise No_graph_found
   in
-  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+  let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
   let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
   let prop_sort = InProp in
   let funs_indexes =
@@ -669,9 +669,9 @@ let build_case_scheme fa =
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_qualid f) in
   let first_fun,u = destConst  funs in
-  let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
+  let funs_mp = Constant.modpath first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
-  let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+  let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
   let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
   let prop_sort = InProp in
   let funs_indexes =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9eda19a86b..9a6169d42a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -898,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) =
 		let id = Label.to_id (Constant.label c) in
                  [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
-	 let mp,dp,_ = Constant.repr3 c in
+         let mp = Constant.modpath c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-           (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+           (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
 	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4eee2c7a45..6ed382ca1c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -297,36 +297,7 @@ let subst_Function (subst,finfos) =
 let classify_Function infos = Libobject.Substitute infos
 
 
-let discharge_Function (_,finfos) =
-  let function_constant' = Lib.discharge_con finfos.function_constant
-  and graph_ind' = Lib.discharge_inductive finfos.graph_ind
-  and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
-  and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
-  and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
-  and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
-  and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
-  and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
-  in
-  if function_constant' == finfos.function_constant &&
-    graph_ind' == finfos.graph_ind &&
-    equation_lemma' == finfos.equation_lemma &&
-    correctness_lemma' == finfos.correctness_lemma &&
-    completeness_lemma' == finfos.completeness_lemma &&
-    rect_lemma' == finfos.rect_lemma &&
-    rec_lemma' == finfos.rec_lemma &&
-    prop_lemma' == finfos.prop_lemma
-  then Some finfos
-  else
-    Some { function_constant = function_constant' ;
-	   graph_ind = graph_ind' ;
-	   equation_lemma = equation_lemma' ;
-	   correctness_lemma = correctness_lemma' ;
-	   completeness_lemma = completeness_lemma';
-	   rect_lemma = rect_lemma';
-	   rec_lemma = rec_lemma';
-	   prop_lemma = prop_lemma' ;
-	   is_general = finfos.is_general
-	 }
+let discharge_Function (_,finfos) = Some finfos
 
 let pr_ocst c =
   let sigma, env = Pfedit.get_current_context () in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad11f853ca..56fe430077 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -450,7 +450,7 @@ let generalize_dependent_of x hyp g =
 let tauto =
   let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
   let mp = ModPath.MPfile (DirPath.make dp) in
-  let kn = KerName.make2 mp (Label.make "tauto") in
+  let kn = KerName.make mp (Label.make "tauto") in
   Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     let body = Tacenv.interp_ltac kn in
     Tacinterp.eval_tactic body
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index c3d063cff8..85081b24a3 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -27,7 +27,7 @@ open Stdarg
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
+  let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in
   let tac = Tacenv.interp_ltac kn in
   Tacinterp.eval_tactic tac
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b05e1e85b7..0734654abf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -266,7 +266,7 @@ let my_reference c =
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
 
 let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -760,7 +760,7 @@ let new_field_path =
   DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))
 
 
 let _ = add_map "field"
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index f23433f2f4..2af917b939 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -337,9 +337,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = destConst elim in
-    let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
+    let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
     let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
-    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
+    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
     mkConst c1', gl in
   let elim = EConstr.of_constr elim in
   let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 53153198f9..8ee6fbf036 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -24,7 +24,6 @@ open Coqlib
 exception Non_closed_ascii
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let is_gr c gr = match DAst.get c with
@@ -32,10 +31,12 @@ let is_gr c gr = match DAst.get c with
 | _ -> false
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
+let ascii_modpath = MPfile (make_dir ascii_module)
 
 let ascii_path = make_path ascii_module "ascii"
 
-let ascii_kn = make_kn ascii_module "ascii"
+let ascii_label = Label.make "ascii"
+let ascii_kn = MutInd.make2 ascii_modpath ascii_label
 let path_of_Ascii = ((ascii_kn,0),1)
 let static_glob_Ascii  = ConstructRef path_of_Ascii
 
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 49497aef54..776d2a2229 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -33,12 +33,10 @@ let is_gr c gr = match DAst.get c with
 | GRef (r, _) -> GlobRef.equal r gr
 | _ -> false
 
+let positive_modpath = MPfile (make_dir binnums)
 let positive_path = make_path binnums "positive"
 
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
+let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
@@ -74,7 +72,7 @@ let rec bignat_of_pos c = match DAst.get c with
 (**********************************************************************)
 
 let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
+let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
 let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
@@ -106,12 +104,10 @@ let bigint_of_z c = match DAst.get c with
 (**********************************************************************)
 
 let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
+let r_modpath = MPfile (make_dir rdefinitions)
 let r_path = make_path rdefinitions "R"
 
-(* TODO: temporary hack *)
-let make_path dir id = Globnames.encode_con dir (Id.of_string id)
-
-let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
+let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
 
 let r_of_int ?loc z =
   DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 7478c1e978..703b40dd3e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -24,9 +24,10 @@ exception Non_closed_string
 
 let string_module = ["Coq";"Strings";"String"]
 
+let string_modpath = MPfile (make_dir string_module)
 let string_path = make_path string_module "string"
 
-let string_kn = make_kn string_module "string"
+let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
 let static_glob_EmptyString  = ConstructRef ((string_kn,0),1)
 let static_glob_String  = ConstructRef ((string_kn,0),2)
 
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index b8958ca944..3da1ab7439 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -46,10 +46,9 @@ let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
        let vars = Lib.variable_section_segment_of_reference c in
-       let c' = pop_global_reference c in
        let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
-       Some (ReqGlobal (c', names), (c', names'))
+       Some (ReqGlobal (c, names), (c, names'))
      with Not_found -> Some req)
   | _ -> None
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b264e31474..b026397abf 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -451,12 +451,6 @@ let subst_coercion (subst, c) =
   else { c with coercion_type = coe; coercion_source = cls;
                 coercion_target = clt; coercion_is_proj = clp; }
 
-let discharge_cl = function
-  | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
-  | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
-  | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
-  | cl -> cl
-
 let discharge_coercion (_, c) =
   if c.coercion_local then None
   else
@@ -467,9 +461,6 @@ let discharge_coercion (_, c) =
       with Not_found -> 0
     in
     let nc = { c with
-      coercion_type = Lib.discharge_global c.coercion_type;
-      coercion_source = discharge_cl c.coercion_source;
-      coercion_target = discharge_cl c.coercion_target;
       coercion_params = n + c.coercion_params;
       coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
     } in
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 7d9debce34..a3e4eb8971 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -14,7 +14,6 @@ open Constr
 open Vars
 open Mod_subst
 open Environ
-open Globnames
 open Libobject
 open Lib
 open Context.Named.Declaration
@@ -171,7 +170,7 @@ let subst_head (subst,(ref,k)) =
 
 let discharge_head (_,(ref,k)) =
   match ref with
-  | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
+  | EvalConstRef cst -> Some (ref, k)
   | EvalVarRef id -> None
 
 let rebuild_head (ref,k) =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 418fdf2a26..4ee7e667fe 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -601,13 +601,13 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = KerName.repr (MutInd.canonical kn) in
+  let mp,l = KerName.repr (MutInd.canonical kn) in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in
+    let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in
     let _ = Global.lookup_constant cst in
       ConstRef cst
   with Not_found ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c25416405e..3719f9302a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -79,12 +79,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 
-let discharge_constructor (ind, n) =
-  (Lib.discharge_inductive ind, n)
-
-let discharge_structure (_,(ind,id,kl,projs)) =
-  Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
-        List.map (Option.map Lib.discharge_con) projs)
+let discharge_structure (_,x) = Some x
 
 let inStruc : struc_tuple -> obj =
   declare_object {(default_object "STRUCTURE") with
@@ -319,8 +314,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
   let ind' = subst_ind subst ind in
   if cst' == cst && ind' == ind then obj else (cst',ind')
 
-let discharge_canonical_structure (_,(cst,ind)) =
-  Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
+let discharge_canonical_structure (_,x) = Some x
 
 let inCanonStruc : Constant.t * inductive -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e8c3b3e2b3..5dbe95a471 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -132,8 +132,7 @@ module ReductionBehaviour = struct
           { b with b_nargs = nargs'; b_recargs = recargs' }
         else b
       in
-      let c = Lib.discharge_con c in
-      Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
+      Some (ReqGlobal (gr, req), (ConstRef c, b))
     | _ -> None
 
   let rebuild = function
@@ -713,8 +712,8 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
   | Name.Name id ->
     let open UnivProblem in
     try
-      let (cst_mod,cst_sect,_) = Constant.repr3 reference in
-      let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
+      let (cst_mod,_) = Constant.repr2 reference in
+      let cst = Constant.make2 cst_mod (Label.of_id id) in
       let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
       match constant_opt_value_in env (cst,u) with
       | None -> bd
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 67c5643459..7e5815acd1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -222,26 +222,26 @@ let discharge_class (_,cl) =
                              | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
 			    ctx'
       in
-      List.Smart.map (Option.Smart.map Lib.discharge_global) grs
-      @ newgrs
+      grs @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
-  let cl_impl' = Lib.discharge_global cl.cl_impl in
-  if cl_impl' == cl.cl_impl then cl else
+  try
     let info = abs_context cl in
     let ctx = info.Lib.abstr_ctx in
     let ctx, subst = rel_of_variable_context ctx in
     let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
     let context = discharge_context ctx (subst, usubst) cl.cl_context in
     let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in
-      { cl_univs = cl_univs';
-        cl_impl = cl_impl';
-	cl_context = context;
-	cl_props = props;
-        cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-	cl_strict = cl.cl_strict;
-	cl_unique = cl.cl_unique
-      }
+    let discharge_proj x = x in
+    { cl_univs = cl_univs';
+      cl_impl = cl.cl_impl;
+      cl_context = context;
+      cl_props = props;
+      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+      cl_strict = cl.cl_strict;
+      cl_unique = cl.cl_unique
+    }
+  with Not_found -> (* not defined in the current section *)
+    cl
 
 let rebuild_class cl = 
   try 
@@ -365,8 +365,8 @@ let discharge_instance (_, (action, inst)) =
     Some (action,
     { inst with 
       is_global = Some (pred n);
-      is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_global inst.is_impl })
+      is_class = inst.is_class;
+      is_impl = inst.is_impl })
     
 
 let is_local i = (i.is_global == None)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 66f748454d..e6f82c60ee 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -617,10 +617,10 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
       | (_,"INDUCTIVE") ->
           Some (gallina_print_inductive (MutInd.make1 kn) None)
       | (_,"MODULE") ->
-	  let (mp,_,l) = KerName.repr kn in
+          let (mp,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
       | (_,"MODULE TYPE") ->
-	  let (mp,_,l) = KerName.repr kn in
+          let (mp,l) = KerName.repr kn in
 	  Some (print_modtype (MPdot (mp,l)))
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
 	    "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
@@ -734,12 +734,12 @@ let print_full_pure_context env sigma =
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = KerName.repr kn in
+          let (mp,l) = KerName.repr kn in
 	  print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | "MODULE TYPE" ->
 	  (* TODO: make it reparsable *)
 	  (* TODO: make it reparsable *)
-	  let (mp,_,l) = KerName.repr kn in
+          let (mp,l) = KerName.repr kn in
 	  print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
       | _ -> mt () in
       prec rest ++ pp
diff --git a/printing/printer.ml b/printing/printer.ml
index cfa3e8b6e9..79654da6e7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -959,7 +959,7 @@ let pr_assumptionset env sigma s =
       try pr_constant env kn
       with Not_found ->
         (* FIXME? *)
-	let mp,_,lab = Constant.repr3 kn in
+        let mp,lab = Constant.repr2 kn in
         str (ModPath.to_string mp) ++ str "." ++ Label.print lab
     in
     let safe_pr_inductive env kn =
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 44685d2bbd..1350da65dc 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -114,9 +114,7 @@ let classify_strategy (local,_ as obj) =
 
 let disch_ref ref =
   match ref with
-      EvalConstRef c ->
-        let c' = Lib.discharge_con c in
-        if c==c' then Some ref else Some (EvalConstRef c')
+      EvalConstRef c -> Some ref
     | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref
 
 let discharge_strategy (_,(local,obj)) =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d0f4b2c680..510f119229 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -356,9 +356,9 @@ let find_elim hdcncl lft2rgt dep cls ot =
         | Some true, None
         | Some false, Some _ ->
 	  let c1 = destConstRef pr1 in 
-	  let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in 
+          let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
 	  let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in 
-	  let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in
+          let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c0ba363360..90eafe88c4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -209,14 +209,14 @@ let fresh_key =
     let cur = incr id; !id in
     let lbl = Id.of_string ("_" ^ string_of_int cur) in
     let kn = Lib.make_kn lbl in
-    let (mp, dir, _) = KerName.repr kn in
+    let (mp, _) = KerName.repr kn in
     (** We embed the full path of the kernel name in the label so that the
         identifier should be unique. This ensures that including two modules
         together won't confuse the corresponding labels. *)
-    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
-      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%i"
+      (ModPath.to_string mp) cur)
     in
-    KerName.make mp dir (Label.of_id lbl)
+    KerName.make mp (Label.of_id lbl)
 
 let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
   let d = pri1 - pri2 in
@@ -1601,7 +1601,7 @@ let warn_non_imported_hint =
 
 let warn env sigma h =
   let hint = pr_hint env sigma h in
-  let (mp, _, _) = KerName.repr h.uid in
+  let mp = KerName.modpath h.uid in
   warn_non_imported_hint (hint,mp)
 
 let wrap_hint_warning t =
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 7da059ae35..a1bb0a7401 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -438,7 +438,7 @@ let match_eq sigma eqn (ref, hetero) =
   | _ -> raise PatternMatchingFailure
 
 let no_check () = true
-let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
+let check_jmeq_loaded () = Library.library_is_loaded @@ Coqlib.jmeq_library_path
 
 let equalities =
   [(coq_eq_ref, false), no_check, build_coq_eq_data;
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e4013152e6..b81967c781 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -56,8 +56,7 @@ let subst_scheme (subst,(kind,l)) =
   (kind,Array.Smart.map (subst_one_scheme subst) l)
 
 let discharge_scheme (_,(kind,l)) =
-  Some (kind,Array.map (fun (ind,const) ->
-    (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
+  Some (kind, l)
 
 let inScheme : string * (inductive * Constant.t) array -> obj =
   declare_object {(default_object "SCHEME") with
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 448febed25..5d53fd2f09 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -225,9 +225,9 @@ Qed.
 (* Illegal application used to make Ltac loop. *)
 
 Section LtacLoopTest.
-  Ltac f x := idtac.
+  Ltac g x := idtac.
   Goal True.
-  Timeout 1 try f()().
+  Timeout 1 try g()().
   Abort.
 End LtacLoopTest.
 
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b000745961..15c0278f47 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -119,7 +119,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x
 
 let lookup_constant_in_impl cst fallback =
   try
-    let mp,dp,lab = KerName.repr (Constant.canonical cst) in
+    let mp,lab = KerName.repr (Constant.canonical cst) in
     let fields = memoize_fields_of_mp mp in
     (* A module found this way is necessarily closed, in particular
        our constant cannot be in an opened section : *)
@@ -143,7 +143,7 @@ let lookup_constant cst =
 
 let lookup_mind_in_impl mind =
   try
-    let mp,dp,lab = KerName.repr (MutInd.canonical mind) in
+    let mp,lab = KerName.repr (MutInd.canonical mind) in
     let fields = memoize_fields_of_mp mp in
       search_mind_label lab fields
   with Not_found ->
@@ -157,9 +157,9 @@ let lookup_mind mind =
     traversed objects *)
 
 let label_of = function
-  | ConstRef kn -> pi3 (Constant.repr3 kn)
+  | ConstRef kn -> Constant.label kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn)
+  | ConstructRef ((kn,_),_) -> MutInd.label kn
   | VarRef id -> Label.of_id id
 
 let fold_constr_with_full_binders g f n acc c =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c738d14af9..37ee33b19f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -99,7 +99,7 @@ let type_ctx_instance env sigma ctx inst subst =
 
 let id_of_class cl =
   match cl.cl_impl with
-    | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l
+    | ConstRef kn -> Label.to_id @@ Constant.label kn
     | IndRef (kn,i) ->
 	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
 	  mip.(0).Declarations.mind_typename
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 015d5fabef..cf2fecb9c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -249,8 +249,7 @@ let print_namespace ns =
   in
   let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
   let print_kn kn =
-    (* spiwack: I'm ignoring the dirpath, is that bad? *)
-    let (mp,_,lbl) = Names.KerName.repr kn in
+    let (mp,lbl) = Names.KerName.repr kn in
     let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
     print_list Id.print qn
   in