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. --- proofs/tacmach.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'proofs/tacmach.ml') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 50984c48e..957843bc9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -21,6 +21,8 @@ open Refiner open Sigma.Notations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + let re_sig it gc = { it = it; sigma = gc; } (**************************************************************) @@ -46,7 +48,7 @@ let pf_hyps_types gls = | LocalDef (id,_,x) -> id, x) sign -let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id let pf_last_hyp gl = List.hd (pf_hyps gl) @@ -57,7 +59,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - pf_get_hyp gls id |> get_type + pf_get_hyp gls id |> NamedDecl.get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -199,7 +201,7 @@ module New = struct sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> get_type + pf_get_hyp id gl |> NamedDecl.get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in -- cgit v1.2.3