diff options
| author | Matej Kosik | 2016-08-13 18:11:22 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-24 21:12:29 +0200 |
| commit | a5d336774c7b5342c8d873d43c9b92bae42b43e7 (patch) | |
| tree | 1a1e4e6868c32222f94ee59257163d7d774ec9d0 /proofs/proof_using.ml | |
| parent | d5d80dfc0f773fd6381ee4efefc74804d103fe4e (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 'proofs/proof_using.ml')
| -rw-r--r-- | proofs/proof_using.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 5b24a1fb23..a125fb10db 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -12,6 +12,8 @@ open Util open Vernacexpr open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let to_string e = let rec aux = function | SsEmpty -> "()" @@ -39,10 +41,10 @@ let rec close_fwd e s = | LocalAssum _ -> Id.Set.empty | LocalDef (_,b,_) -> global_vars_set e b in - let vty = global_vars_set e (get_type decl) in + let vty = global_vars_set e (NamedDecl.get_type decl) in let vbty = Id.Set.union vb vty in if Id.Set.exists (fun v -> Id.Set.mem v s) vbty - then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s) + then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s) s (named_context e) in if Id.Set.equal s s' then s else close_fwd e s' @@ -65,13 +67,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id and full_set env = - List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in |