From fd7f056b155b2ebaafa3251a3c136117ebefc3e3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 May 2017 11:48:51 +0200
Subject: Cleanup: removal of constr_of_global.

Constrintern.pf_global returns a global_reference, not a constr,
adapt plugins accordingly, properly registering universes where
necessary.
---
 vernac/vernacentries.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c1d64cfe9..036173c6d7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1765,12 +1765,11 @@ let vernac_locate = let open Feedback in function
 let vernac_register id r =
  if Pfedit.refining () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let t = (Constrintern.global_reference (snd id)) in
-  if not (isConst t) then
+  let kn = Constrintern.global_reference (snd id) in
+  if not (isConstRef kn) then
     user_err Pp.(str "Register inline: a constant is expected");
-  let kn = destConst t in
   match r with
-  | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
+  | RegisterInline -> Global.register_inline (destConstRef kn)
 
 (********************)
 (* Proof management *)
-- 
cgit v1.2.3