[kernel] Remove section paths from `KerName.t`

We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.

Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.

14 files changed, 39 insertions, 71 deletions

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)