[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.

1 files changed, 1 insertions, 2 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0efb27e3f0..08298bf02c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -14,7 +14,6 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
-open Globnames
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -1027,7 +1026,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
               update_Function
                 {finfos with
                    equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                                              ConstRef c -> c
+                                              GlobRef.ConstRef c -> c
                                             | _ -> CErrors.anomaly (Pp.str "Not a constant.")
                                          )
                 }