From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001
From: Matej Kosik <matej.kosik@inria.fr>
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.
---
 pretyping/tacred.ml | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'pretyping/tacred.ml')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 820a81b5d..c1d4a3403 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -25,6 +25,9 @@ open Patternops
 open Locus
 open Sigma.Notations
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Errors *)
 
 type reduction_tactic_error =
@@ -54,13 +57,12 @@ let is_evaluable env = function
   | EvalVarRef id -> is_evaluable_var env id
 
 let value_of_evaluable_ref env evref u =
-  let open Context.Named.Declaration in
   match evref with
   | EvalConstRef con -> 
     (try constant_value_in env (con,u)
     with NotEvaluableConst IsProj -> 
       raise (Invalid_argument "value_of_evaluable_ref"))
-  | EvalVarRef id -> lookup_named id env |> get_value |> Option.get
+  | EvalVarRef id -> lookup_named id env |> NamedDecl.get_value |> Option.get
 
 let evaluable_of_global_reference env = function
   | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
@@ -112,22 +114,18 @@ let unsafe_reference_opt_value env sigma eval =
     | Declarations.Def c -> Some (Mod_subst.force_constr c)
     | _ -> None)
   | EvalVar id ->
-      let open Context.Named.Declaration in
-      lookup_named id env |> get_value
+      lookup_named id env |> NamedDecl.get_value
   | EvalRel n ->
-      let open Context.Rel.Declaration in
-      lookup_rel n env |> map_value (lift n) |> get_value
+      lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 let reference_opt_value env sigma eval u = 
   match eval with
   | EvalConst cst -> constant_opt_value_in env (cst,u)
   | EvalVar id ->
-      let open Context.Named.Declaration in
-      lookup_named id env |> get_value
+      lookup_named id env |> NamedDecl.get_value
   | EvalRel n ->
-      let open Context.Rel.Declaration in
-      lookup_rel n env |> map_value (lift n) |> get_value
+      lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
   | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable
@@ -541,11 +539,9 @@ let match_eval_ref_value env sigma constr =
   | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
     Some (constant_value_in env (sp, u))
   | Var id when is_evaluable env (EvalVarRef id) -> 
-     let open Context.Named.Declaration in
-     lookup_named id env |> get_value
+     lookup_named id env |> NamedDecl.get_value
   | Rel n ->
-     let open Context.Rel.Declaration in
-     lookup_rel n env |> map_value (lift n) |> get_value
+     lookup_rel n env |> RelDecl.map_value (lift n) |> RelDecl.get_value
   | Evar ev -> Evd.existential_opt_value sigma ev
   | _ -> None
 
-- 
cgit v1.2.3