From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 13 Jun 2018 00:22:57 +0200
Subject: Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.
---
 interp/constrextern.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 73c108319f..f09b316cd6 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -38,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -56,9 +56,9 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit
 val get_extern_reference :
-  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid)
 
 (** WARNING: The following functions are evil due to
     side-effects. Think of the following case as used in the printer:
-- 
cgit v1.2.3