[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.

4 files changed, 10 insertions, 39 deletions

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