From c51fb2fae0e196012de47203b8a71c61720d6c5c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Jun 2019 22:50:08 +0200
Subject: [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.
---
 doc/plugin_tutorial/tuto1/src/simple_print.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'doc/plugin_tutorial/tuto1/src')

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
-- 
cgit v1.2.3