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.

1 files changed, 8 insertions, 7 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b54e2badd..83ad9af33 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -96,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
     else l
   in
   let rec aux bdvars l c = match CAst.(c.v) with
-    | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
-        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | CRef (qid,_) when qualid_is_ident qid ->
+      found c.CAst.loc (qualid_basename qid) bdvars l
+    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+        qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
+        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
@@ -196,7 +198,7 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, decl) ->
     let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
+      (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
 
 let destClassApp cl =
   let open CAst in
@@ -218,9 +220,8 @@ let destClassAppExpl cl =
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
-      let qid = qualid_of_reference r in
-      let gr = Nametab.locate qid.CAst.v in
+      let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
+      let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in