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/subtyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bfe68671a2..d64342dbb0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,8 @@ let check_polymorphic_instance error env auctx1 auctx2 =
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
-  let kn1 = KerName.make2 mp1 l in
-  let kn2 = KerName.make2 mp2 l in
+  let kn1 = KerName.make mp1 l in
+  let kn2 = KerName.make mp2 l in
   let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst poly f = check_conv_error error why cst poly f in
   let mib1 =
-- 
cgit v1.2.3