(** creates an opaque tactic from a status->proof*goal list function *)
let mk_tactic t = t
+type pattern = (string * Cic.term) list * Cic.term option
+let goal_pattern = [],None
+
(** tactic failure *)
exception Fail of string
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 =