None -> assert false
| Some (uri,metasenv,bo,ty) ->
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
None -> assert false
| Some (uri,metasenv,bo,ty) ->
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)