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.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/constrintern.mli') diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe57..644f60d85 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