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. --- library/lib.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 7fc3e0d9c..412772e8a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,6 +13,9 @@ open Libnames open Globnames open Nameops open Libobject +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) @@ -428,9 +431,8 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = - let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -443,8 +445,7 @@ let extract_hyps (secs,ohyps) = in aux (secs,ohyps) let instance_from_variable_context = - let open Context.Named.Declaration in - Array.of_list % List.map get_id % List.filter is_local_assum % List.map fst + Array.of_list % List.map NamedDecl.get_id % List.filter is_local_assum % List.map fst let named_of_variable_context = List.map fst -- cgit v1.2.3