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 /pretyping/find_subterm.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 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e992..1f9573862 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -16,6 +16,8 @@ open Nameops open Termops open Pretype_errors +module NamedDecl = Context.Named.Declaration + (** Processing occurrences *) type occurrence_error = @@ -61,7 +63,7 @@ let proceed_with_occurrences f occs x = let map_named_declaration_with_hyploc f hyploc acc decl = let open Context.Named.Declaration in - let f = f (Some (get_id decl, hyploc)) in + let f = f (Some (NamedDecl.get_id decl, hyploc)) in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> error_occurrences_error (IncorrectInValueOccurrence id) |