(** an unfinished proof with the optional current goal *)
type tactic = status -> proof * goal list
+ (** creates an opaque tactic from a status->proof*goal list function *)
+let mk_tactic t = t
+
(** tactic failure *)
exception Fail of string
+ (**
+ 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)
+
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name