(** creates an opaque tactic from a status->proof*goal list function *)
let mk_tactic t = t
+ (** what, hypothesis patterns, conclusion pattern *)
+type pattern = Cic.term option * (string * Cic.term) list * Cic.term
+let conclusion_pattern t = t,[],Cic.Implicit (Some `Hole)
+
(** 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 =