From 650c65af484c45f4e480252b55d148bcc198be6c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 25 Sep 2018 14:33:46 +0200
Subject: [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.
---
 printing/prettyp.ml | 8 ++++----
 printing/printer.ml | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing')

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 =
-- 
cgit v1.2.3