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.

7 files changed, 33 insertions, 40 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a158fc8ff..31496513a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -627,7 +627,7 @@ let build_scheme fas =
 		Smartlocate.global_with_alias f
 	      with Not_found ->
                 user_err ~hdr:"FunInd.build_scheme"
-                  (str "Cannot find " ++ Libnames.pr_reference f)
+                  (str "Cannot find " ++ Libnames.pr_qualid f)
 	    in
             let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
@@ -668,7 +668,7 @@ let build_case_scheme fa =
     try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
-        (str "Cannot find " ++ Libnames.pr_reference f) in
+        (str "Cannot find " ++ Libnames.pr_qualid f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 33aeafef8..97f9acdb3 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -36,5 +36,5 @@ exception No_graph_found
 val make_scheme :   Evd.evar_map ref ->
  (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
 
-val build_scheme : (Id.t*Libnames.reference*Sorts.family) list ->  unit
-val build_case_scheme : (Id.t*Libnames.reference*Sorts.family)  ->  unit
+val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
+val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 9899b7b21..a2d31780d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -168,7 +168,7 @@ END
 
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
   Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
-  Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
+  Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
   Termops.pr_sort_family s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
@@ -181,11 +181,11 @@ let warning_error names e =
   let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-       let names = pr_enum Libnames.pr_reference names in
+       let names = pr_enum Libnames.pr_qualid names in
        let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
        warn_cannot_define_graph (names,error)
     | Defining_principle e ->
-       let names = pr_enum Libnames.pr_reference names in
+       let names = pr_enum Libnames.pr_qualid names in
        let error = if do_observe () then CErrors.print e else mt () in
        warn_cannot_define_principle (names,error)
     | _ -> raise e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cd640eebd..489a40ed0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-        let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in
+        let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in
 	let ind_kn =
 	  fst (locate_with_msg
-		 (pr_reference f_R_mut++str ": Not an inductive type!")
+                 (pr_qualid f_R_mut++str ": Not an inductive type!")
 		 locate_ind
 		 f_R_mut)
 	in
 	let fname_kn (((fname,_),_,_,_,_),_) =
-          let f_ref = CAst.map (fun n -> Ident n) fname in
-	  locate_with_msg
-	    (pr_reference f_ref++str ": Not an inductive type!")
+   let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
+          locate_with_msg
+            (pr_qualid f_ref++str ": Not an inductive type!")
 	    locate_constant
 	    f_ref
 	in
@@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let unbounded_eq =
     let f_app_args =
       CAst.make @@ Constrexpr.CAppExpl(
-         (None,CAst.make @@ Ident fname,None) ,
+         (None,qualid_of_ident fname,None) ,
 	 (List.map
 	    (function
                | {CAst.v=Anonymous} -> assert false
@@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-            CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path
-			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
-	  in
+            Libnames.qualid_of_path
+              (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))
+          in
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
@@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   ()
 
 let rec add_args id new_args = CAst.map (function
-  | CRef (r,_) as b ->
-      begin match r with
-        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
-	    CAppExpl((None,r,None),new_args)
-	| _ -> b
-      end
+  | CRef (qid,_) as b ->
+    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+      CAppExpl((None,qid,None),new_args)
+    else b
   | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
   | CProdN(nal,b1) ->
         CProdN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
@@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function
 	       add_args id new_args  b1)
   | CLetIn(na,b1,t,b2) ->
       CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
-  | CAppExpl((pf,r,us),exprl) ->
-      begin
-	match r with
-        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
-	    CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
-      end
+  | CAppExpl((pf,qid,us),exprl) ->
+    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+      CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl))
+    else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl)
   | CApp((pf,b),bl) ->
       CApp((pf,add_args id new_args b),
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
@@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) =
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
                                         (fun {CAst.loc;v=n} -> CAst.make ?loc @@
-                                           CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None))
+                                           CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
 			       )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6faa142a..4eee2c7a4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -31,9 +31,7 @@ let id_of_name = function
     Name id -> id
   | _ -> raise Not_found
 
-let locate  ref =
-    let {CAst.v=qid} = qualid_of_reference ref in
-    Nametab.locate qid
+let locate qid = Nametab.locate qid
 
 let locate_ind ref =
   match locate ref with
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 346b21ef2..7e52ee224 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array
 
 val id_of_name : Name.t -> Id.t
 
-val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> Constant.t
+val locate_ind : Libnames.qualid -> inductive
+val locate_constant : Libnames.qualid -> Constant.t
 val locate_with_msg :
-  Pp.t -> (Libnames.reference -> 'a) ->
-  Libnames.reference -> 'a
+  Pp.t -> (Libnames.qualid -> 'a) ->
+  Libnames.qualid -> 'a
 
 val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
 val list_union_eq :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index aa49148fc..7298342e1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =
     let opacity =
-      let na_ref = CAst.make @@ Libnames.Ident na in
+      let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
@@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in
+    let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);