From 9edb5777f08f338367cd4384abdc17efcf2c2892 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 11:04:57 +0200
Subject: Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)

This is the only use of restrict_path so we just remove it.

The name collision between Libnames.make_path (takes a dirpath) and
Lib.make_path (uses current module+section path) is a bit awkward...
---
 library/libnames.ml  | 5 -----
 library/libnames.mli | 2 --
 2 files changed, 7 deletions(-)

(limited to 'library')

diff --git a/library/libnames.ml b/library/libnames.ml
index 18af216e46..485f8837e8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -128,11 +128,6 @@ let path_of_string s =
 
 let pr_path sp = str (string_of_path sp)
 
-let restrict_path n sp =
-  let dir, s = repr_path sp in
-  let dir' = List.firstn n (DirPath.repr dir) in
-  make_path (DirPath.make dir') s
-
 (*s qualified names *)
 type qualid_r = full_path
 type qualid = qualid_r CAst.t
diff --git a/library/libnames.mli b/library/libnames.mli
index 4455e29818..ffd7032fff 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -57,8 +57,6 @@ val pr_path : full_path -> Pp.t
 
 module Spmap  : CSig.MapS with type key = full_path
 
-val restrict_path : int -> full_path -> full_path
-
 (** {6 ... } *)
 (** A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
-- 
cgit v1.2.3


From d324c858be652659a5062332f00e7d20393a48be Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 12:35:49 +0200
Subject: Safe_typing.push_named_assum: don't take universes

The caller should push them first
---
 library/global.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index 51307b3604..d034bc4208 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -38,7 +38,7 @@ val sprop_allowed : unit -> bool
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
 
 val export_private_constants : in_section:bool ->
-- 
cgit v1.2.3