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, 6 insertions, 6 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6e01a676a..8c43ac8b5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -32,6 +32,8 @@ open Misctypes
 open Proofview.Notations
 open Hints
 
+module NamedDecl = Context.Named.Declaration
+
 (** Hint database named "typeclass_instances", now created directly in Auto *)
 
 (** Options handling *)
@@ -523,9 +525,8 @@ let evars_to_goals p evm =
 
 (** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
-  let open Context.Named.Declaration in
-  let id = get_id decl in
-  let cty = Evarutil.nf_evar sigma (get_type decl) in
+  let id = NamedDecl.get_id decl in
+  let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum ty in
       match kind_of_term (fst (decompose_app ar)) with
@@ -564,10 +565,9 @@ let make_hints g st only_classes sign =
     List.fold_left
       (fun hints hyp ->
         let consider =
-          let open Context.Named.Declaration in
-          try let t = Global.lookup_named (get_id hyp) |> get_type in
+          try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in
               (* Section variable, reindex only if the type changed *)
-              not (Term.eq_constr t (get_type hyp))
+              not (Term.eq_constr t (NamedDecl.get_type hyp))
           with Not_found -> true
         in
         if consider then