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/refiner.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/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ebd30820b..d9ab2fbdb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,7 +13,8 @@ open Evd open Environ open Proof_type open Logic -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -202,7 +203,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) let { it = gls; sigma = sigma; } = rslt in let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,7 +216,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in Feedback.msg_notice |