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.
---
 interp/implicit_quantifiers.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 10cfbe58fa..4d9386b9da 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -21,6 +21,8 @@ open Libobject
 open Nameops
 open Misctypes
 open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 (*i*)
 
 let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
@@ -198,7 +200,7 @@ let combine_params avoid fn applied needed =
     List.partition
       (function
 	  (t, Some (loc, ExplByName id)) ->
-            let is_id (_, decl) = match get_name decl with
+            let is_id (_, decl) = match RelDecl.get_name decl with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
             in
@@ -242,7 +244,7 @@ let combine_params avoid fn applied needed =
 
 let combine_params_freevar =
   fun avoid (_, decl) ->
-    let id' = next_name_away_from (get_name decl) avoid in
+    let id' = next_name_away_from (RelDecl.get_name decl) avoid in
       (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
 
 let destClassApp cl =
-- 
cgit v1.2.3