From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 13 Aug 2016 18:11:22 +0200
Subject: 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.
---
 stm/lemmas.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'stm')

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index fb2f0351d2..5e4e341146 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -33,6 +33,9 @@ open Constrintern
 open Impargs
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
 let mk_hook hook = hook
 let call_hook fix_exn hook l c =
@@ -45,8 +48,7 @@ let call_hook fix_exn hook l c =
 
 let retrieve_first_recthm = function
   | VarRef id ->
-      let open Context.Named.Declaration in
-      (get_value (Global.lookup_named id),variable_opacity id)
+      (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
       (Global.body_of_constant_body cb, is_opaque cb)
@@ -110,7 +112,7 @@ let find_mutually_recursive_statements thms =
         (Global.env()) hyps in
       let ind_hyps =
         List.flatten (List.map_i (fun i decl ->
-          let t = get_type decl in
+          let t = RelDecl.get_type decl in
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
@@ -456,7 +458,7 @@ let start_proof_com kind thms hook =
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
-    let ids = List.map get_name ctx in
+    let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
-- 
cgit v1.2.3