Merge PR #10498: [api] Deprecate GlobRef constructors.

Reviewed-by: SkySkimmer
Ack-by: ppedrot

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