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 /plugins/funind/glob_term_to_relation.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 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02fe6ce3a..4d02c77c8 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -366,7 +366,6 @@ let add_pat_variables pat typ env : Environ.env = Context.Rel.fold_outside (fun decl (env,ctxt) -> let open Context.Rel.Declaration in - (*let _,v,t = Context.Rel.Declaration.to_tuple decl in*) match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> @@ -415,8 +414,7 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let open Context.Rel.Declaration in - let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -615,7 +613,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = - let open Context.Named.Declaration in match n with Anonymous -> env | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env @@ -989,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let open Context.Rel.Declaration in - let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in + let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> |