CLEANUP: minor readability improvements

mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.

If multiple modules define a function with a same name, e.g.:

	Context.{Rel,Named}.get_type

those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.

1 files changed, 4 insertions, 3 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb5..a74fceb8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -34,7 +34,8 @@ open Tacred
 open Printer
 open Vernacexpr
 open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (****************************************)
 (* General functions                    *)
@@ -782,11 +783,11 @@ let make_resolves env sigma flags pri poly ?name cr =
 
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma decl =
-  let hname = get_id decl in
+  let hname = NamedDecl.get_id decl in
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (mkVar hname, get_type decl, Univ.ContextSet.empty)]
+       (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")