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.
---
 interp/constrintern.ml  | 6 +++---
 interp/constrintern.mli | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..628c85e755 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -98,16 +98,16 @@ let global_reference_of_reference ref =
   locate_reference (snd (qualid_of_reference ref))
 
 let global_reference id =
-  Universes.constr_of_global (locate_reference (qualid_of_ident id))
+  locate_reference (qualid_of_ident id)
 
 let construct_reference ctx id =
   try
-    Term.mkVar (let _ = Context.Named.lookup id ctx in id)
+    VarRef (let _ = Context.Named.lookup id ctx in id)
   with Not_found ->
     global_reference id
 
 let global_reference_in_absolute_module dir id =
-  Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+  Nametab.global_of_path (Libnames.make_path dir id)
 
 (**********************************************************************)
 (* Internalization errors                                             *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644cafe575..644f60d850 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -176,9 +176,9 @@ val interp_context_evars :
 
 val locate_reference :  Libnames.qualid -> Globnames.global_reference
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr
-val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
+val global_reference : Id.t -> Globnames.global_reference
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)
-- 
cgit v1.2.3