[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.

1 files changed, 5 insertions, 4 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index ba989b1bac..88afec14d5 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/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