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.
---
 plugins/omega/coq_omega.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6aec83318c..3b79a130f2 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -27,7 +27,6 @@ open Tacmach.New
 open Tactics
 open Logic
 open Libnames
-open Globnames
 open Nametab
 open Contradiction
 open Tactypes
@@ -426,11 +425,11 @@ let destructurate_prop sigma t =
     | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
     | Const (sp,_), args ->
-	Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args)
     | Construct (csp,_) , args ->
-	Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args)
     | Ind (isp,_), args ->
-	Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body)
     | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
-- 
cgit v1.2.3