+ (**
+ calls the opaque tactic on the status, restoring the original
+ universe graph if the tactic Fails
+ *)
+let apply_tactic t status =
+ let saved_univ = CicUniv.get_working() in
+ try
+ t status
+ with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+