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/setoid_ring/newring.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9973f2ec1d..eb75fca0a1 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -49,7 +49,7 @@ let global_head_of_constr sigma c =
 
 let global_of_constr_nofail c = 
   try global_of_constr c
-  with Not_found -> VarRef (Id.of_string "dummy")
+  with Not_found -> GlobRef.VarRef (Id.of_string "dummy")
 
 let rec mk_clos_but f_map n t =
   let (f, args) = Constr.decompose_appvect t in
-- 
cgit v1.2.3