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

(limited to 'printing/printer.ml')

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