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

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index e550e06471..dbf570eaad 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -301,7 +301,7 @@ type section_variable_entry =
 
 type variable_declaration = DirPath.t * section_variable_entry
 
-let cache_variable ((sp,_),o) =
+let cache_variable (_,o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
   | Inr (id,(path,d),kind) ->
@@ -339,7 +339,7 @@ let cache_variable ((sp,_),o) =
       let () = Global.push_named_def (id, se) in
       Decl_kinds.Explicit, de.proof_entry_opaque,
       poly, univs in
-  Nametab.push (Nametab.Until 1) (Libnames.restrict_path 0 sp) (GlobRef.VarRef id);
+  Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty id) (GlobRef.VarRef id);
   add_section_variable ~name:id ~kind:impl ~poly univs;
   Decls.(add_variable_data id {path;opaque;univs;poly;kind})
 
-- 
cgit v1.2.3