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.
---
 engine/termops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 1ed2d93b3c..2ab2f60421 100644
--- a/engine/termops.ml
+++ b/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
-- 
cgit v1.2.3