aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-08-13 18:11:22 +0200
committerMatej Kosik2016-08-24 21:12:29 +0200
commita5d336774c7b5342c8d873d43c9b92bae42b43e7 (patch)
tree1a1e4e6868c32222f94ee59257163d7d774ec9d0 /interp/implicit_quantifiers.ml
parentd5d80dfc0f773fd6381ee4efefc74804d103fe4e (diff)
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.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
-rw-r--r--interp/implicit_quantifiers.ml6
1 files changed, 4 insertions, 2 deletions
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 =