(** 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
"elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
- if not (are_convertible context t1'' t1) then begin
+ let b,_ = (*TASSI : FIXME*)
+ are_convertible context t1'' t1 CicUniv.empty_ugraph in
+ if not b then begin
warn "t1'' and t1 are NOT CONVERTIBLE";
let newstatus =
ProofEngineTypes.apply_tactic
ProofEngineTypes.mk_tactic (fun status ->
let status' =
let context = context_of_status status in
- if not (are_convertible context t2'' t2) then begin
+ let b,_ = (* TASSI:FIXME *)
+ are_convertible context t2'' t2 CicUniv.empty_ugraph
+ in
+ if not b then begin
warn "t2'' and t2 are NOT CONVERTIBLE";
let newstatus =
ProofEngineTypes.apply_tactic