diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-08-13 18:11:22 +0200 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2016-08-24 21:12:29 +0200 |
| commit | a5d336774c7b5342c8d873d43c9b92bae42b43e7 (patch) | |
| tree | 1a1e4e6868c32222f94ee59257163d7d774ec9d0 /proofs/proof_global.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_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7605f6387..4cb9f03ce 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -18,6 +18,8 @@ open Util open Pp open Names +module NamedDecl = Context.Named.Declaration + (*** Proof Modes ***) (* Type of proof modes : @@ -276,7 +278,7 @@ let set_used_variables l = let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with |