(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("RING WARNING: " ^ s)
+ debug_print ("RING WARNING: " ^ s)
(** CIC URIS *)
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