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)
+ t status
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =