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.
---
 kernel/nativecode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativecode.ml')

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