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/names.mli | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index 2ea8108734..2145a51c4e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -274,9 +274,11 @@ sig
   type t
 
   (** Constructor and destructor *)
-  val make : ModPath.t -> DirPath.t -> Label.t -> t
+  val make : ModPath.t -> Label.t -> t
+  val repr : t -> ModPath.t * Label.t
+
   val make2 : ModPath.t -> Label.t -> t
-  val repr : t -> ModPath.t * DirPath.t * Label.t
+  [@@ocaml.deprecated "Please use [KerName.make]"]
 
   (** Projections *)
   val modpath : t -> ModPath.t
@@ -317,15 +319,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
@@ -403,15 +402,12 @@ sig
   val make2 : ModPath.t -> Label.t -> t
   (** Shortcut for [(make1 (KerName.make2 ...))] *)
 
-  val make3 : ModPath.t -> DirPath.t -> Label.t -> t
-  (** Shortcut for [(make1 (KerName.make ...))] *)
-
   (** Projections *)
 
   val user : t -> KerName.t
   val canonical : t -> KerName.t
 
-  val repr3 : t -> ModPath.t * DirPath.t * Label.t
+  val repr2 : t -> ModPath.t * Label.t
   (** Shortcut for [KerName.repr (user ...)] *)
 
   val modpath : t -> ModPath.t
-- 
cgit v1.2.3