diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 8d6bdf6ae..186525e15 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -13,7 +13,7 @@ open Evd open Environ open Proof_type open Logic - +open Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -202,7 +202,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 (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in + let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,7 +215,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 (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in pp (str (emacs_str "<infoH>") |