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.
---
 dev/doc/changes.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index fdeb0abed4..5371d84a06 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -7,6 +7,17 @@ Termops:
 - Internal printing functions have been placed under the
   `Termops.Internal` namespace.
 
+Names
+
+- Kernel names no longer contain a section path. They now have only two
+  components (module path and label), which led to some changes in the API:
+
+  KerName.make takes only 2 components
+  KerName.repr returns only 2 components
+  KerName.make2 is now KerName.make
+  Constant.make3 has been removed, use Constant.make2
+  Constant.repr3 has been removed, use Constant.repr2
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
-- 
cgit v1.2.3