[api] Deprecate GlobRef constructors.

Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.

I have taken the opportunity to reduce the number of `open` in the
codebase.

The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.

dev/top_printers.ml

@@ -15,7 +15,6 @@ open Util
 open Pp
 open Names
 open Libnames
-open Globnames
 open Univ
 open Environ
 open Printer
@@ -141,7 +140,7 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
 
 let pP s = pp (hov 0 s)
 
-let safe_pr_global = function
+let safe_pr_global = let open GlobRef in function
   | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")")
   | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++
 			  int i ++ str ")")
@@ -558,7 +557,7 @@ let encode_path ?loc prefix mpdir suffix id =
   make_qualid ?loc
     (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
-let raw_string_of_ref ?loc _ = function
+let raw_string_of_ref ?loc _ = let open GlobRef in function
   | ConstRef cst ->
       let (mp,id) = Constant.repr2 cst in
       encode_path ?loc "CST" (Some mp) [] (Label.to_id id)
@@ -574,7 +573,7 @@ let raw_string_of_ref ?loc _ = function
   | VarRef id ->
       encode_path ?loc "SECVAR" None [] id
 
-let short_string_of_ref ?loc _ = function
+let short_string_of_ref ?loc _ = let open GlobRef in function
   | VarRef id -> qualid_of_ident ?loc id
   | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst))
   | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn))

doc/plugin_tutorial/tuto1/src/simple_print.ml

@@ -2,14 +2,15 @@
   type constr is given in the coq-dpdgraph plugin. *)
 
 let simple_body_access gref =
+  let open Names.GlobRef in
   match gref with
-  | Globnames.VarRef _ ->
+  | VarRef _ ->
     failwith "variables are not covered in this example"
-  | Globnames.IndRef _ ->
+  | IndRef _ ->
     failwith "inductive types are not covered in this example"
-  | Globnames.ConstructRef _ ->
+  | ConstructRef _ ->
     failwith "constructors are not covered in this example"
-  | Globnames.ConstRef cst ->
+  | ConstRef cst ->
     let cb = Environ.lookup_constant cst (Global.env()) in
     match Global.body_of_constant_body Library.indirect_accessor cb with
     | Some(e, _, _) -> EConstr.of_constr e

engine/namegen.ml

@@ -24,7 +24,6 @@ open EConstr
 open Vars
 open Nameops
 open Libnames
-open Globnames
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -72,7 +71,7 @@ let is_imported_modpath = function
     in find_prefix (Lib.current_mp ())
   | _ -> false
 
-let is_imported_ref = function
+let is_imported_ref = let open GlobRef in function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
@@ -90,7 +89,7 @@ let is_global id =
 let is_constructor id =
   try
     match Nametab.locate (qualid_of_ident id) with
-      | ConstructRef _ -> true
+      | GlobRef.ConstructRef _ -> true
       | _ -> false
   with Not_found ->
     false
@@ -102,7 +101,7 @@ let is_section_variable id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
-let global_of_constr = function
+let global_of_constr = let open GlobRef in function
 | Const (c, _) -> ConstRef c
 | Ind (i, _) -> IndRef i
 | Construct (c, _) -> ConstructRef c
@@ -149,8 +148,8 @@ let hdchar env sigma c =
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
     | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
-    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
-    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->

engine/termops.ml

@@ -1058,7 +1058,7 @@ let is_section_variable id =
   with Not_found -> false
 
 let global_of_constr sigma c =
-  let open Globnames in
+  let open GlobRef in
   match EConstr.kind sigma c with
   | Const (c, u) -> ConstRef c, u
   | Ind (i, u) -> IndRef i, u
@@ -1067,7 +1067,7 @@ let global_of_constr sigma c =
   | _ -> raise Not_found
 
 let is_global sigma c t =
-  let open Globnames in
+  let open GlobRef in
   match c, EConstr.kind sigma t with
   | ConstRef c, Const (c', _) -> Constant.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
@@ -1379,7 +1379,7 @@ let dependency_closure env sigma sign hyps =
     List.rev lh
 
 let global_app_of_constr sigma c =
-  let open Globnames in
+  let open GlobRef in
   match EConstr.kind sigma c with
   | Const (c, u) -> (ConstRef c, u), None
   | Ind (i, u) -> (IndRef i, u), None

engine/univGen.ml

@@ -56,15 +56,15 @@ let fresh_global_instance ?loc ?names env gr =
   u, ctx
 
 let fresh_constant_instance env c =
-  let u, ctx = fresh_global_instance env (ConstRef c) in
+  let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
   (c, u), ctx
 
 let fresh_inductive_instance env ind =
-  let u, ctx = fresh_global_instance env (IndRef ind) in
+  let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
   (ind, u), ctx
 
 let fresh_constructor_instance env c =
-  let u, ctx = fresh_global_instance env (ConstructRef c) in
+  let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
   (c, u), ctx
 
 let fresh_global_instance ?loc ?names env gr =
@@ -84,10 +84,10 @@ let fresh_global_or_constr_instance env = function
 
 let global_of_constr c =
   match kind c with
-  | Const (c, u) -> ConstRef c, u
-  | Ind (i, u) -> IndRef i, u
-  | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Instance.empty
+  | Const (c, u) -> GlobRef.ConstRef c, u
+  | Ind (i, u) -> GlobRef.IndRef i, u
+  | Construct (c, u) -> GlobRef.ConstructRef c, u
+  | Var id -> GlobRef.VarRef id, Instance.empty
   | _ -> raise Not_found
 
 let fresh_sort_in_family = function

interp/constrextern.ml

@@ -16,7 +16,6 @@ open Names
 open Nameops
 open Termops
 open Libnames
-open Globnames
 open Namegen
 open Impargs
 open CAst
@@ -361,7 +360,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
   if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
-  let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
+  let impl_st = extract_impargs_data (implicits_of_global (GlobRef.ConstructRef c)) in
   let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
@@ -416,22 +415,22 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 		          (* we don't want to have 'x := _' in our patterns *)
                           acc
 		       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc)
+                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
                        | _ -> raise No_match in
                      ip q tail acc
 	          | _ -> assert false
 	      in
 	      CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-                  let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in
+                  let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (c, None, args)
 		    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
-		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
+                    match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with
 		      | Some true_args -> CPatCstr (c, None, true_args)
 		      | None           -> CPatCstr (c, Some full_args, [])
           in
@@ -500,7 +499,7 @@ and extern_notation_pattern allscopes vars t = function
       match DAst.get t with
         | PatCstr (cstr,args,na) ->
           let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
-	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
+          let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr)
             (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias ?loc p na
 	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
@@ -513,7 +512,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
   | (keyrule,pat,n as _rule)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
-      apply_notation_to_pattern (IndRef ind)
+      apply_notation_to_pattern (GlobRef.IndRef ind)
         (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
         No_match -> extern_notation_ind_pattern allscopes vars ind args rules
@@ -522,7 +521,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
-    let c = extern_reference vars (IndRef ind) in
+    let c = extern_reference vars (GlobRef.IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
@@ -531,9 +530,9 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
       extern_notation_ind_pattern allscopes vars ind args
           (uninterp_ind_pattern_notations ind)
     with No_match ->
-      let c = extern_reference vars (IndRef ind) in
+      let c = extern_reference vars (GlobRef.IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
-      match drop_implicits_in_patt (IndRef ind) 0 args with
+      match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with
 	   |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
 	   |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
@@ -825,7 +824,7 @@ let rec extern inctx scopes vars r =
 	     begin
 	       try
                  if !Flags.raw_print then raise Exit;
-		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
+                 let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
 		 let struc = Recordops.lookup_structure (fst cstrsp) in
                  if PrintingRecord.active (fst cstrsp) then
                    ()
@@ -858,7 +857,7 @@ let rec extern inctx scopes vars r =
 				     (* we give up since the constructor is not complete *)
 				 | (arg, scopes) :: tail ->
                                      let head = extern true scopes vars arg in
-                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
+                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
 		   in
 		 CRecord (List.rev (ip projs locals args []))
 	       with
@@ -1238,7 +1237,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
-  | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
+  | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
 			 [glob_of_pat avoid env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)