match (n, context) with
| (0, _) -> status
| (n, hd::tl) ->
- aux (n-1) tl
- (status_of_single_goal_tactic_result
- (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
+ let name_of_hyp =
+ match hd with
+ None
+ | Some (Cic.Anonymous,_) -> assert false
+ | Some (Cic.Name name,_) -> name
+ in
+ aux (n-1) tl
+ (status_of_single_goal_tactic_result
+ (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in